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

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

(92 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

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

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

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

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

(14 entries)

Global Index

A

AbstractMSO [library]
accept [definition, in FinTypes.Automata]
accepting [definition, in OAut.Buechi]
accepting_all [lemma, in OAut.NecessityAR]
accepting_proper [instance, in OAut.Buechi]
accepting_extensional [lemma, in OAut.Buechi]
accepting_run_for_W' [lemma, in OAut.Complement]
accepting_implies_less [lemma, in OAut.MSO]
accepting_run_less [lemma, in OAut.MSO]
accepting_run_search_Y [lemma, in OAut.MSO]
accepting_applies_incl [lemma, in OAut.MSO]
accept_dec [instance, in FinTypes.Automata]
acc_dec [instance, in FinTypes.Automata]
activeW [definition, in OAut.Buechi]
ADD [definition, in OAut.Ramsey]
add [projection, in OAut.Ramsey]
addEqClass [definition, in OAut.Complement]
addEqClass_is_associative [lemma, in OAut.Complement]
addEqClass_is_additive [lemma, in OAut.Complement]
AdditiveRamsey [definition, in OAut.Ramsey]
AdditiveRamsey [section, in OAut.Ramsey]
additiveRamsey_implies_mso_classical [lemma, in OAut.NecessityAR]
additiveRamsey_implies_compl [lemma, in OAut.NecessityAR]
additive_ramsey_iff_ramsey_fac [lemma, in OAut.NecessityAR]
ADD_formula_correct [lemma, in OAut.NecessityAR]
ADD_formula [definition, in OAut.NecessityAR]
ADD_formula'_correct [lemma, in OAut.NecessityAR]
ADD_formula' [definition, in OAut.NecessityAR]
ADD_extract_last [lemma, in OAut.Ramsey]
ADD_single_extract [lemma, in OAut.Ramsey]
ADD_iter [lemma, in OAut.Ramsey]
ADD_split [lemma, in OAut.Ramsey]
ADD_Proper [instance, in OAut.Ramsey]
ADD' [definition, in OAut.Ramsey]
ADD'_last [lemma, in OAut.Ramsey]
ADD'_extensional [lemma, in OAut.Ramsey]
admissible [definition, in FinTypes.FinTypes]
AdmissibleSequenceStructure [record, in OAut.ASStructures]
admits_ramseyan_fac_iff_idem_ramseyan_fac [lemma, in OAut.Ramsey]
admits_idempotent_ramseyan_factorization [definition, in OAut.Ramsey]
admits_ramseyan_factorization [definition, in OAut.Ramsey]
allSub [lemma, in FinTypes.FinTypes]
all_finite_impossible [lemma, in OAut.NecessityAR]
all_fin_nfa_correct [lemma, in OAut.NecessityAR]
all_fin_nfa [definition, in OAut.NecessityAR]
all_not_nfa_correct [lemma, in OAut.NecessityAR]
all_not_nfa [definition, in OAut.NecessityAR]
all_not_a [abbreviation, in OAut.NecessityAR]
all1_correct [lemma, in OAut.AbstractMSO]
all2_correct [lemma, in OAut.AbstractMSO]
amap [projection, in OAut.ASStructures]
amap_proper [instance, in OAut.ASStructures]
amap_correct [projection, in OAut.ASStructures]
And [constructor, in OAut.AbstractMSO]
and_dec [instance, in FinTypes.External]
and_correct [lemma, in OAut.AbstractMSO]
appendNil [lemma, in FinTypes.BasicDefinitions]
applyVect [definition, in FinTypes.FinTypes]
apply_vectorise_inverse [lemma, in FinTypes.FinTypes]
app_equi_proper [instance, in FinTypes.External]
app_incl_proper [instance, in FinTypes.External]
APreImage [definition, in OAut.ASStructures]
ARC [definition, in OAut.MSO]
ASeq [projection, in OAut.ASStructures]
aseq_run [projection, in OAut.ASStructures]
aseq_equal_equiv [instance, in OAut.ASStructures]
aseq_equal [definition, in OAut.ASStructures]
aseq_to_seq [projection, in OAut.ASStructures]
Assoc [projection, in OAut.Ramsey]
associative [definition, in OAut.Ramsey]
ASStructures [library]
at_least_one_nfa_correct [lemma, in OAut.NecessityAR]
at_least_one_nfa [definition, in OAut.NecessityAR]
at_most_one_eq_class [lemma, in OAut.Complement]
autC_disjoint [lemma, in OAut.ASStructures]
Automata [library]
autU_accepted_by_aut1 [lemma, in OAut.Buechi]
aut_accepts_normalize [lemma, in OAut.RegularLanguages]
aut_accepts_nfa_omega_iter' [lemma, in OAut.Buechi]
aut_accepts_image [lemma, in OAut.Buechi]
aut1_incl_autU [lemma, in OAut.Buechi]
azip [projection, in OAut.ASStructures]
azip_correct [projection, in OAut.ASStructures]

B

BasicDefinitions [library]
BasicDefs [library]
begin_in_equal [lemma, in OAut.Seqs]
begin_in [definition, in OAut.Seqs]
between_final_state_intersect_is_final_state_aut_1 [lemma, in OAut.Buechi]
bigAnd [definition, in OAut.AbstractMSO]
bigAndCorrect [lemma, in OAut.AbstractMSO]
bigEx2 [definition, in OAut.AbstractMSO]
bigEx2_correct [lemma, in OAut.AbstractMSO]
bigOr [definition, in OAut.AbstractMSO]
bigOrCorrect [lemma, in OAut.AbstractMSO]
bigpi [definition, in OAut.ASStructures]
bigpi_correct [lemma, in OAut.ASStructures]
bigUpdate2 [definition, in OAut.AbstractMSO]
bigUpdate2Spec [definition, in OAut.AbstractMSO]
bigUpdate2_update [lemma, in OAut.AbstractMSO]
bigUpdate2_unchanged [lemma, in OAut.AbstractMSO]
bigzip [definition, in OAut.ASStructures]
BigZip [section, in OAut.ASStructures]
bigzip_correct [lemma, in OAut.ASStructures]
bigzip_correct' [lemma, in OAut.ASStructures]
bigzip' [definition, in OAut.ASStructures]
_ ==== _ [notation, in OAut.ASStructures]
big_intersection_scorrect [lemma, in OAut.RegularLanguages]
big_sintersection [definition, in OAut.RegularLanguages]
big_intersection_compl_correct [lemma, in OAut.NecessityAR]
big_intersection_correct [lemma, in OAut.Buechi]
big_intersection [definition, in OAut.Buechi]
big_union_correct [lemma, in OAut.Buechi]
big_union [definition, in OAut.Buechi]
big_union_acorrect [lemma, in OAut.ASStructures]
big_and_false [lemma, in OAut.Ramsey]
big_and_true [lemma, in OAut.Ramsey]
bijective [definition, in FinTypes.BasicDefinitions]
boolOption_enum_ok [lemma, in FinTypes.FinTypes]
bool_eq_dec [instance, in FinTypes.External]
bool_enum_ok [lemma, in FinTypes.FinTypes]
bot [definition, in OAut.AbstractMSO]
bot_correct [lemma, in OAut.AbstractMSO]
bounded_path_iff_path [lemma, in OAut.NFAs]
bounded_run_is_valid_path [lemma, in OAut.NFAs]
bounded_unchanged_string [lemma, in OAut.Seqs]
bounded_unchanged [lemma, in OAut.Seqs]
bounded_strict_forall [instance, in OAut.FinType]
bounded_exist [instance, in OAut.FinType]
bounded_forall [instance, in OAut.FinType]
bounded_type_exist [instance, in OAut.FinType]
Buechi [library]
BuechiAutomaton [section, in OAut.Buechi]
BuechiAutomaton.aut [variable, in OAut.Buechi]
BuechiEquivalenceRelation [section, in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable [section, in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsFinalRecognizable [section, in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsFinalRecognizable.endS [variable, in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsFinalRecognizable.startS [variable, in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsRecognizable [section, in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsRecognizable.endS [variable, in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsRecognizable.startS [variable, in OAut.Complement]
BuechiEquivalenceRelation.BuechiEquivalenceClassRecognizableMyhillNerode [section, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility [section, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.Acc [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.agree_R [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.agree_r0 [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.eqLengthv [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.inV [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.inV' [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.inW [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.inW' [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.R [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.r0 [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.V [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.v [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.valid_R [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.valid_r0 [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.v' [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.W [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.w [variable, in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.w' [variable, in OAut.Complement]
BuechiEquivalenceRelation.Totality [section, in OAut.Complement]
_ ~~ _ [notation, in OAut.Complement]
_ =!=> _ on _ [notation, in OAut.Complement]
_ ===> _ on _ [notation, in OAut.Complement]
{[ _ ]} [notation, in OAut.Complement]
buechi_language_proper [instance, in OAut.Buechi]
buechi_language [definition, in OAut.Buechi]
buechi_equiv_class_NFA_recognizable [lemma, in OAut.Complement]
buechi_equiv_class_aut [definition, in OAut.Complement]
buechi_equiv_class_NFA_recognizable_MyhillNerode [lemma, in OAut.Complement]
buechi_eq_class_proper [instance, in OAut.Complement]
buechi_equiv [abbreviation, in OAut.Complement]
buechi_eq_class_correct [lemma, in OAut.Complement]
buechi_eq_class [definition, in OAut.Complement]

C

cancat_strings_proper [instance, in OAut.Seqs]
can_find_duplicate' [lemma, in OAut.Seqs]
can_find_duplicate [lemma, in OAut.Seqs]
can_find_next_position [lemma, in OAut.Seqs]
card [definition, in FinTypes.External]
CardIn [lemma, in FinTypes.FinTypes]
Cardinality [section, in FinTypes.External]
Cardinality [definition, in FinTypes.FinTypes]
Cardinality_card_eq [lemma, in FinTypes.FinTypes]
Cardinality.X [variable, in FinTypes.External]
card_equi_proper [instance, in FinTypes.External]
card_or [lemma, in FinTypes.External]
card_lt [lemma, in FinTypes.External]
card_equi [lemma, in FinTypes.External]
card_ex [lemma, in FinTypes.External]
card_0 [lemma, in FinTypes.External]
card_cons_rem [lemma, in FinTypes.External]
card_eq [lemma, in FinTypes.External]
card_le [lemma, in FinTypes.External]
card_not_in_rem [lemma, in FinTypes.External]
card_in_rem [lemma, in FinTypes.External]
card_upper_bound [lemma, in FinTypes.FinTypes]
Card_positiv [lemma, in FinTypes.FinTypes]
Card_X_eq [definition, in FinTypes.FinTypes]
card_length_leq [lemma, in FinTypes.BasicDefinitions]
card_finType_Le_K [lemma, in OAut.FinType]
card_finTypeC_Le_K [lemma, in OAut.FinType]
CC [projection, in OAut.ASStructures]
cc_nat [lemma, in OAut.BasicDefs]
cc_nat_first [lemma, in OAut.BasicDefs]
class [projection, in FinTypes.FinTypes]
ClassicalReasoning [section, in OAut.AbstractMSO]
classifier [definition, in OAut.Complement]
Closure [lemma, in FinTypes.FinTypes]
ClosureProperties [section, in OAut.RegularLanguages]
ClosureProperties [section, in OAut.ASStructures]
ClosureProperties.AC [variable, in OAut.ASStructures]
ClosureProperties.Complement [section, in OAut.ASStructures]
ClosureProperties.ComplementCorollaries [section, in OAut.ASStructures]
ClosureProperties.Complement.aut [variable, in OAut.ASStructures]
ClosureProperties.X [variable, in OAut.ASStructures]
ClosureProperties.Y [variable, in OAut.ASStructures]
ClosureUnderComplementImpliesAdditiveRamsey [section, in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.complement [variable, in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.RamseyNFA [section, in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.RamseyNFA.RamseyNFAIdem [section, in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.RamseyNFA.RamseyNFAIdem.x [variable, in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.xm_word_problem [variable, in OAut.NecessityAR]
closure_complement_implies_finite_type_seq [lemma, in OAut.NecessityAR]
Closure_FCIter [lemma, in FinTypes.FinTypes]
coincidence [lemma, in OAut.AbstractMSO]
coloring_additive [definition, in OAut.Ramsey]
combine_final_transforms_right [lemma, in OAut.Complement]
combine_final_transforms_left [lemma, in OAut.Complement]
combine_transforms [lemma, in OAut.Complement]
compact_f [lemma, in OAut.Ramsey]
compatibility [lemma, in OAut.Complement]
compatibilityComplement [lemma, in OAut.Complement]
compatibility2 [lemma, in OAut.Complement]
ComplClosed [definition, in OAut.NecessityAR]
complement [definition, in FinTypes.Automata]
complement [definition, in OAut.Complement]
Complement [section, in OAut.Complement]
Complement [library]
complement_correct [lemma, in FinTypes.Automata]
complement_auts [definition, in OAut.Complement]
complement_correct2 [lemma, in OAut.ASStructures]
complement_correct [lemma, in OAut.ASStructures]
complement_complete [lemma, in OAut.ASStructures]
Complement.A [variable, in OAut.Complement]
Complement.aut [variable, in OAut.Complement]
complete_induction [lemma, in OAut.BasicDefs]
compl_closed_xm_word_problem_implies_ramsey_fac [lemma, in OAut.NecessityAR]
compose_s_monotone [lemma, in OAut.Seqs]
compute_run_final_transforms [lemma, in OAut.Complement]
compute_run_transforms [lemma, in OAut.Complement]
conact_delta_dec [instance, in FinTypes.Automata]
concat [definition, in FinTypes.Automata]
ConcatInfPrependNFA [section, in OAut.Buechi]
ConcatInfPrependNFA.runs [variable, in OAut.Buechi]
ConcatInfPrependNFA.strings [variable, in OAut.Buechi]
concat_paths [lemma, in OAut.NFAs]
concat_inf_is_valid' [lemma, in OAut.NFAs]
concat_inf_is_valid [lemma, in OAut.NFAs]
concat_inf_is_valid'' [lemma, in OAut.NFAs]
concat_map_length [lemma, in FinTypes.FinTypes]
concat_correct [lemma, in FinTypes.Automata]
concat_delta_Q_star_correct4 [lemma, in FinTypes.Automata]
concat_delta_Q_star_correct3 [lemma, in FinTypes.Automata]
concat_delta_Q_star_correct2 [lemma, in FinTypes.Automata]
concat_delta_Q_star_correct1 [lemma, in FinTypes.Automata]
concat_delta_Q [definition, in FinTypes.Automata]
concat_delta [definition, in FinTypes.Automata]
concat_acc_decPred [definition, in FinTypes.Automata]
concat_acc_pred [definition, in FinTypes.Automata]
concat_inf_infiniteP_inverse [lemma, in OAut.Seqs]
concat_inf_infiniteP [lemma, in OAut.Seqs]
concat_strings_omega_unfold [lemma, in OAut.Seqs]
concat_inf_indices_constant_step' [lemma, in OAut.Seqs]
concat_inf_indices_constant_step [lemma, in OAut.Seqs]
concat_inf_indices_constant_first [lemma, in OAut.Seqs]
concat_inf_indices_step [lemma, in OAut.Seqs]
concat_inf_extensional [lemma, in OAut.Seqs]
concat_inf_index_equal [lemma, in OAut.Seqs]
concat_inf_correct [lemma, in OAut.Seqs]
concat_inf_index_to_begin [lemma, in OAut.Seqs]
concat_inf_index_injective [lemma, in OAut.Seqs]
concat_if_indices_lower_bound [lemma, in OAut.Seqs]
concat_inf_index_le [lemma, in OAut.Seqs]
concat_inf_index_step_correct [lemma, in OAut.Seqs]
concat_inf_index_in_bounds [lemma, in OAut.Seqs]
concat_inf_index_correct [lemma, in OAut.Seqs]
concat_inf_index_begin [lemma, in OAut.Seqs]
concat_inf_index_in_string [lemma, in OAut.Seqs]
concat_inf [definition, in OAut.Seqs]
concat_inf_indices [definition, in OAut.Seqs]
concat_extract [lemma, in OAut.Seqs]
concat_strings_associative [lemma, in OAut.Seqs]
concat_prepend_string_associative [lemma, in OAut.Seqs]
concat_strings_length [lemma, in OAut.Seqs]
concat_strings_step [lemma, in OAut.Seqs]
concat_string_rest [lemma, in OAut.Seqs]
concat_string_begin [lemma, in OAut.Seqs]
concat_strings [definition, in OAut.Seqs]
cons [definition, in FinTypes.Automata]
consAppend [lemma, in FinTypes.BasicDefinitions]
const [definition, in OAut.ASStructures]
ConstLengthString [definition, in OAut.Seqs]
constSeq [definition, in OAut.MSO]
constStr [definition, in OAut.MSO]
const_correct [lemma, in OAut.ASStructures]
cons_equi_proper [instance, in FinTypes.External]
cons_incl_proper [instance, in FinTypes.External]
cons_correct [lemma, in FinTypes.Automata]
cons_incll [lemma, in FinTypes.BasicDefinitions]
ConvertToNFA [section, in OAut.RegularLanguages]
ConvertToNFA.aut [variable, in OAut.RegularLanguages]
convRemInv [definition, in OAut.FinType]
convRemInv_seqToInter [lemma, in OAut.MSO]
convRemInv_correct' [lemma, in OAut.FinType]
convRemInv_correct [lemma, in OAut.FinType]
count [definition, in FinTypes.BasicDefinitions]
countApp [lemma, in FinTypes.BasicDefinitions]
countIn [lemma, in FinTypes.BasicDefinitions]
countMap [lemma, in FinTypes.BasicDefinitions]
countMapExistT [lemma, in FinTypes.FinTypes]
countMapExistT_Zero [lemma, in FinTypes.FinTypes]
countMapZero [lemma, in FinTypes.BasicDefinitions]
countNumberApp [lemma, in FinTypes.FinTypes]
countSplit [lemma, in FinTypes.BasicDefinitions]
counttFL [lemma, in FinTypes.FinTypes]
countZero [lemma, in FinTypes.BasicDefinitions]
count_in_equiv [lemma, in FinTypes.BasicDefinitions]
Cover [definition, in OAut.MSO]
cover_correct [lemma, in OAut.MSO]
create_Le_K [definition, in OAut.FinType]
critical_index_unfold_distance' [lemma, in OAut.ASStructures]
critical_index_unfold_distance [lemma, in OAut.ASStructures]
critical_index_unfold_pred_index [lemma, in OAut.ASStructures]
critical_index_unfold_ge_zero [lemma, in OAut.ASStructures]
critical_index_unfold_monotone [lemma, in OAut.ASStructures]
critical_index_unfold_bound [lemma, in OAut.ASStructures]
critical_index [definition, in OAut.ASStructures]
critical_index_unfold [definition, in OAut.ASStructures]
cut [definition, in OAut.Seqs]
cut_loop_preserves_last_state [lemma, in OAut.NFAs]
cut_loop_preserves_first_state [lemma, in OAut.NFAs]
cut_loop_decrease [lemma, in OAut.NFAs]
cut_loop_valid [lemma, in OAut.NFAs]
cut_loop [definition, in OAut.NFAs]
cut_rest [lemma, in OAut.Seqs]
cut_front [lemma, in OAut.Seqs]
cut_string_cut [lemma, in OAut.Seqs]
cut_string [definition, in OAut.Seqs]
cycle_omega_is_valid_run [lemma, in OAut.NFAs]

D

dec [definition, in FinTypes.External]
decActivW [instance, in OAut.Buechi]
DecBuechiAutomatonEmpty [section, in OAut.Buechi]
DecBuechiAutomatonEmpty.aut [variable, in OAut.Buechi]
DecConnected [section, in OAut.NFAs]
decide_rel [projection, in FinTypes.External]
decide_pred [projection, in FinTypes.External]
decide_eq [projection, in FinTypes.External]
decision [definition, in FinTypes.External]
decision_false [lemma, in OAut.BasicDefs]
decision_true [lemma, in OAut.BasicDefs]
decMemSet [projection, in OAut.AbstractMSO]
decMemSetInstance [instance, in OAut.AbstractMSO]
decPred [record, in FinTypes.External]
DecPred [constructor, in FinTypes.External]
decp_dec [instance, in FinTypes.External]
DecRef [lemma, in FinTypes.BasicDefinitions]
decRel [record, in FinTypes.External]
DecRel [constructor, in FinTypes.External]
decRel_dec [instance, in FinTypes.External]
dec_prop_iff [lemma, in FinTypes.External]
dec_DM_all [lemma, in FinTypes.External]
dec_DM_impl [lemma, in FinTypes.External]
dec_DM_and' [lemma, in FinTypes.External]
dec_DM_and [lemma, in FinTypes.External]
dec_DN [lemma, in FinTypes.External]
dec_trans [lemma, in FinTypes.External]
dec_norm_transition [instance, in OAut.RegularLanguages]
dec_saccepting [instance, in OAut.RegularLanguages]
dec_sfinal [instance, in OAut.RegularLanguages]
dec_sinitial [instance, in OAut.RegularLanguages]
dec_svalid [instance, in OAut.RegularLanguages]
dec_transition_all [instance, in OAut.NecessityAR]
dec_transition_at_least_one [instance, in OAut.NecessityAR]
dec_ramset_transition [instance, in OAut.NecessityAR]
dec_connected [instance, in OAut.NFAs]
dec_valid_path [instance, in OAut.NFAs]
dec_singleton_sets [lemma, in OAut.AbstractMSO]
dec_even [instance, in OAut.AbstractMSO]
dec_up_in_lang [lemma, in OAut.Buechi]
dec_prepend_state_final [instance, in OAut.Buechi]
dec_prepend_transition [instance, in OAut.Buechi]
dec_intersection_transition [instance, in OAut.Buechi]
dec_intersection_final [instance, in OAut.Buechi]
dec_intersection_initial [instance, in OAut.Buechi]
dec_union_final [instance, in OAut.Buechi]
dec_union_initial [instance, in OAut.Buechi]
dec_union_transition [instance, in OAut.Buechi]
dec_language_empty [lemma, in OAut.Buechi]
dec_language_empty_informative [lemma, in OAut.Buechi]
dec_language_empty_informative_periodic [lemma, in OAut.Buechi]
dec_VW_part_of_complement [instance, in OAut.Complement]
dec_pure_W_final [instance, in OAut.Complement]
dec_buechi_eq_class [instance, in OAut.Complement]
dec_transforms_final [instance, in OAut.Complement]
dec_transforms [instance, in OAut.Complement]
dec_pair_eq [instance, in OAut.MSO]
dec_satisfaction_up [lemma, in OAut.MSO]
dec_up_in_lang' [lemma, in OAut.MSO]
dec_general_sat [lemma, in OAut.MSO]
dec_up_sat [lemma, in OAut.MSO]
dec_sat [lemma, in OAut.MSO]
dec_less_transition [instance, in OAut.MSO]
dec_incl_transition [instance, in OAut.MSO]
dec_ciritcal_index [instance, in OAut.ASStructures]
dec_critical_index_unfold [instance, in OAut.ASStructures]
dec_language_eq [lemma, in OAut.ASStructures]
dec_language_inclusion [lemma, in OAut.ASStructures]
dec_language_universal [lemma, in OAut.ASStructures]
dec_alanguage_empty [lemma, in OAut.ASStructures]
dec_alanguage_empty_informative [projection, in OAut.ASStructures]
dec_smallest [instance, in OAut.FinType]
dec_pure_le_k_public [instance, in OAut.FinType]
dec_pure_le_k [instance, in OAut.FinType]
dec_le_k [instance, in OAut.FinType]
dec_merge_at [instance, in OAut.Ramsey]
deltaCons [definition, in FinTypes.Automata]
delta_Q_star_trans [lemma, in FinTypes.Automata]
delta_Q_star_dec [instance, in FinTypes.Automata]
delta_Q_star [definition, in FinTypes.Automata]
delta_Q [projection, in FinTypes.Automata]
delta_star_reach [lemma, in FinTypes.Automata]
delta_star [definition, in FinTypes.Automata]
delta_S [projection, in FinTypes.Automata]
DeriveRamseyFac [section, in OAut.Ramsey]
DeriveRamseyFac.ConstructiveChoiceNcrossN [section, in OAut.Ramsey]
DeriveRamseyFac.f [variable, in OAut.Ramsey]
DeriveRamseyFac.INF_DM [variable, in OAut.Ramsey]
DeriveRamseyFac.IPP_DM [variable, in OAut.Ramsey]
_ ~~# _ [notation, in OAut.Ramsey]
_ ~~@ _ at _ [notation, in OAut.Ramsey]
detlaQstar_convert_inverse [lemma, in OAut.RegularLanguages]
detlaQstar_convert [lemma, in OAut.RegularLanguages]
detlaQstar_decrease_step [lemma, in OAut.RegularLanguages]
dev_prepend_state_initial [instance, in OAut.Buechi]
dfa [record, in FinTypes.Automata]
DFA [constructor, in FinTypes.Automata]
DFA [section, in FinTypes.Automata]
DFA.Operations [section, in FinTypes.Automata]
DFA.Operations.A [variable, in FinTypes.Automata]
DFA.Operations.A' [variable, in FinTypes.Automata]
DFA.Operations.Product_automaton.op_dec [variable, in FinTypes.Automata]
DFA.Operations.Product_automaton.op [variable, in FinTypes.Automata]
DFA.Operations.Product_automaton [section, in FinTypes.Automata]
DFA.Reachability [section, in FinTypes.Automata]
DFA.Reachability.A [variable, in FinTypes.Automata]
DFA.Sig [variable, in FinTypes.Automata]
diff [definition, in FinTypes.Automata]
diff_correct [lemma, in FinTypes.Automata]
disjoint [definition, in FinTypes.External]
disjoint_app [lemma, in FinTypes.External]
disjoint_cons [lemma, in FinTypes.External]
disjoint_nil' [lemma, in FinTypes.External]
disjoint_nil [lemma, in FinTypes.External]
disjoint_incl [lemma, in FinTypes.External]
disjoint_symm [lemma, in FinTypes.External]
disjoint_forall [lemma, in FinTypes.External]
disjoint_in_map_map_cons [lemma, in FinTypes.FinTypes]
disjoint_in [lemma, in FinTypes.FinTypes]
disjoint_map_cons [lemma, in FinTypes.FinTypes]
disjoint_concat [lemma, in FinTypes.FinTypes]
divToV1 [lemma, in OAut.AbstractMSO]
divToV2 [lemma, in OAut.AbstractMSO]
DM_not_exists [lemma, in FinTypes.External]
DM_or [lemma, in FinTypes.External]
DM_exists [lemma, in FinTypes.FinTypes]
DM_notAll [lemma, in FinTypes.FinTypes]
drop [definition, in OAut.Seqs]
drop_preserves_infinite [lemma, in OAut.Seqs]
drop_preserves_infiniteP [lemma, in OAut.Seqs]
drop_proper [instance, in OAut.Seqs]
drop_extract [lemma, in OAut.Seqs]
drop_string_end [definition, in OAut.Seqs]
drop_string_begin [definition, in OAut.Seqs]
drop_correct'' [lemma, in OAut.Seqs]
drop_correct' [lemma, in OAut.Seqs]
drop_correct [lemma, in OAut.Seqs]
dummy [lemma, in OAut.Seqs]
Dupfree [section, in FinTypes.External]
dupfree [inductive, in FinTypes.External]
dupfreeC [constructor, in FinTypes.External]
dupfreeCount [lemma, in FinTypes.BasicDefinitions]
DupFreeDis [section, in FinTypes.External]
DupFreeDis.X [variable, in FinTypes.External]
dupfreeN [constructor, in FinTypes.External]
dupfree_in_power [lemma, in FinTypes.External]
dupfree_power [lemma, in FinTypes.External]
dupfree_undup [lemma, in FinTypes.External]
dupfree_card [lemma, in FinTypes.External]
dupfree_dec [lemma, in FinTypes.External]
dupfree_filter [lemma, in FinTypes.External]
dupfree_map [lemma, in FinTypes.External]
dupfree_app [lemma, in FinTypes.External]
dupfree_cons [lemma, in FinTypes.External]
dupfree_FCIter [lemma, in FinTypes.FinTypes]
dupfree_iterstep [lemma, in FinTypes.FinTypes]
dupfree_FCStep [lemma, in FinTypes.FinTypes]
dupfree_concat_map_cons [lemma, in FinTypes.FinTypes]
dupfree_concat [lemma, in FinTypes.FinTypes]
dupfree_length [lemma, in FinTypes.FinTypes]
dupfree_elements [lemma, in FinTypes.FinTypes]
dupfree_countOne [lemma, in FinTypes.FinTypes]
dupfree_injective_map [lemma, in OAut.FinType]
Dupfree.X [variable, in FinTypes.External]

E

econcat [definition, in OAut.Complement]
EisEquivProper [instance, in OAut.FinType]
elem [definition, in FinTypes.FinTypes]
elementIn [lemma, in FinTypes.FinTypes]
elements [projection, in OAut.Ramsey]
elemToFinType [definition, in OAut.ASStructures]
el_correct [lemma, in OAut.AbstractMSO]
empty [definition, in FinTypes.Automata]
EmptyBuechiAutomaton [section, in OAut.Buechi]
Empty_set_enum_ok [lemma, in FinTypes.FinTypes]
empty_reach [lemma, in FinTypes.Automata]
empty_dec [instance, in FinTypes.Automata]
empty_aut_correct [lemma, in OAut.Buechi]
empty_aut [definition, in OAut.Buechi]
Empty_set_eq_dec [instance, in FinTypes.BasicDefinitions]
empty_aut_acorrect [lemma, in OAut.ASStructures]
empty_language [definition, in OAut.BasicDefs]
enum [projection, in FinTypes.FinTypes]
enum_ok_fromList [lemma, in FinTypes.FinTypes]
enum_ok [projection, in FinTypes.FinTypes]
Epsilon_autom_correct [lemma, in FinTypes.Automata]
Epsilon_autom [definition, in FinTypes.Automata]
EqBool [definition, in FinTypes.BasicDefinitions]
eqClass [definition, in OAut.Complement]
EqClass [definition, in OAut.Complement]
EqClassPair [abbreviation, in OAut.Complement]
EqEmpty_set [definition, in FinTypes.BasicDefinitions]
EqFalse [definition, in FinTypes.BasicDefinitions]
EqLe_K [definition, in OAut.FinType]
EqList [definition, in FinTypes.BasicDefinitions]
EqNat [definition, in FinTypes.BasicDefinitions]
EqOption [definition, in FinTypes.BasicDefinitions]
EqProd [definition, in FinTypes.BasicDefinitions]
EqSigT [definition, in FinTypes.BasicDefinitions]
EqSubType [definition, in FinTypes.BasicDefinitions]
EqSum [definition, in FinTypes.BasicDefinitions]
EqTrue [definition, in FinTypes.BasicDefinitions]
eqtype [projection, in FinTypes.External]
eqType [record, in FinTypes.External]
EqType [constructor, in FinTypes.External]
equalSELangImpliesEqualSLang [lemma, in OAut.Complement]
Equi [section, in FinTypes.External]
equi [definition, in FinTypes.External]
Equivalence_property_exists' [lemma, in FinTypes.FinTypes]
Equivalence_property_exists [lemma, in FinTypes.FinTypes]
Equivalence_property_all [lemma, in FinTypes.FinTypes]
equivalence_class_extensional_proper [instance, in OAut.Complement]
equivalence_class_closed_proper [instance, in OAut.Complement]
equivalent_in_equivalence_class [lemma, in OAut.Complement]
equivalent_in_equivalence_class' [lemma, in OAut.Complement]
equiv_unsat [lemma, in OAut.AbstractMSO]
equiv_eq_dec [instance, in FinTypes.Automata]
equiv_class [definition, in OAut.FinType]
equiv_merge_subseq_merge_at_next [lemma, in OAut.Ramsey]
equiv_merge_subseq_s_monotone [lemma, in OAut.Ramsey]
equiv_merge_subseq [definition, in OAut.Ramsey]
equi_rotate [lemma, in FinTypes.External]
equi_shift [lemma, in FinTypes.External]
equi_swap [lemma, in FinTypes.External]
equi_dup [lemma, in FinTypes.External]
equi_push [lemma, in FinTypes.External]
equi_Equivalence [instance, in FinTypes.External]
Equi.X [variable, in FinTypes.External]
EqUnit [definition, in FinTypes.BasicDefinitions]
EqVect [definition, in FinTypes.FinTypes]
eq_iff [lemma, in FinTypes.FinTypes]
eq_dec_sigT [instance, in FinTypes.BasicDefinitions]
eq_funTrans [lemma, in FinTypes.BasicDefinitions]
eq_classes_extensional [lemma, in OAut.Complement]
eq_string_access' [lemma, in OAut.Seqs]
eq_string_access [lemma, in OAut.Seqs]
EString [definition, in OAut.Complement]
exactW [definition, in FinTypes.Automata]
exactW_correct [lemma, in FinTypes.Automata]
exact_up_nfa_correct [lemma, in OAut.Buechi]
exact_up_nfa [definition, in OAut.Buechi]
exact_at_correct [projection, in OAut.ASStructures]
exact_at [projection, in OAut.ASStructures]
Example1 [definition, in FinTypes.FinTypes]
Example1 [definition, in FinTypes.FinTypes]
Example2 [definition, in FinTypes.FinTypes]
Example2 [definition, in FinTypes.FinTypes]
exists_not_accept_dec [instance, in FinTypes.Automata]
exists_accept_dec [instance, in FinTypes.Automata]
expl [definition, in FinTypes.FinTypes]
extensionalPower [definition, in FinTypes.FinTypes]
External [library]
extPow_length [lemma, in FinTypes.FinTypes]
extract [definition, in OAut.Seqs]
extract_omega_iter [lemma, in OAut.Seqs]
extract_concat_inf [lemma, in OAut.Seqs]
extract_proper [instance, in OAut.Seqs]
extract_prepend [lemma, in OAut.Seqs]
extract_from_drop' [lemma, in OAut.Seqs]
extract_from_drop [lemma, in OAut.Seqs]
extract_correct [lemma, in OAut.Seqs]

F

F [abbreviation, in OAut.NecessityAR]
F [projection, in FinTypes.Automata]
F [abbreviation, in OAut.Ramsey]
FAll [definition, in OAut.AbstractMSO]
False_dec [instance, in FinTypes.External]
False_enum_ok [lemma, in FinTypes.FinTypes]
False_eq_dec [instance, in FinTypes.BasicDefinitions]
FCIter [definition, in FinTypes.FinTypes]
FCIter_ind [lemma, in FinTypes.FinTypes]
FCIter_fp [lemma, in FinTypes.FinTypes]
FCStep [definition, in FinTypes.FinTypes]
FCStep_admissible [lemma, in FinTypes.FinTypes]
FEx [constructor, in OAut.AbstractMSO]
filter [definition, in FinTypes.External]
FilterLemmas [section, in FinTypes.External]
FilterLemmas_pq.q [variable, in FinTypes.External]
FilterLemmas_pq.p [variable, in FinTypes.External]
FilterLemmas_pq.X [variable, in FinTypes.External]
FilterLemmas_pq [section, in FinTypes.External]
FilterLemmas.p [variable, in FinTypes.External]
FilterLemmas.X [variable, in FinTypes.External]
filter_comm [lemma, in FinTypes.External]
filter_and [lemma, in FinTypes.External]
filter_pq_eq [lemma, in FinTypes.External]
filter_pq_mono [lemma, in FinTypes.External]
filter_fst' [lemma, in FinTypes.External]
filter_fst [lemma, in FinTypes.External]
filter_app [lemma, in FinTypes.External]
filter_id [lemma, in FinTypes.External]
filter_mono [lemma, in FinTypes.External]
filter_incl [lemma, in FinTypes.External]
final [definition, in OAut.Buechi]
final_dec_public [instance, in OAut.NFAs]
final_state_dec [projection, in OAut.NFAs]
final_state [projection, in OAut.NFAs]
final_loop_implies_up_seq [lemma, in OAut.Buechi]
final_loop_exists [definition, in OAut.Buechi]
final_iff_step [lemma, in OAut.Buechi]
final_prepend [lemma, in OAut.Buechi]
final_drop [lemma, in OAut.Buechi]
final_r' [lemma, in OAut.Complement]
final_transform_implies_transform [lemma, in OAut.Complement]
final_to_critical [lemma, in OAut.ASStructures]
final_state_eq [lemma, in OAut.ASStructures]
finBigAnd [definition, in OAut.AbstractMSO]
finBigAndCorrect [lemma, in OAut.AbstractMSO]
finBigEx2 [definition, in OAut.AbstractMSO]
finBigEx2_correct [lemma, in OAut.AbstractMSO]
finBigOr [definition, in OAut.AbstractMSO]
finBigOrCorrect [lemma, in OAut.AbstractMSO]
finBigUpdate2 [definition, in OAut.AbstractMSO]
finBigUpdate2_changed [lemma, in OAut.AbstractMSO]
finBigUpdate2_unchanged [lemma, in OAut.AbstractMSO]
FindNextPosition [section, in OAut.Seqs]
FindNextPosition.NextPosition [section, in OAut.Seqs]
FindNextPosition.NextPositionExists [section, in OAut.Seqs]
FindNextPosition.NextPositionExists.L [variable, in OAut.Seqs]
FindNextPosition.NextPosition.F [variable, in OAut.Seqs]
FindNextPosition.NextPosition.L [variable, in OAut.Seqs]
FindNextPosition.P [variable, in OAut.Seqs]
FindNextPosition.w [variable, in OAut.Seqs]
fInduction [lemma, in FinTypes.FinTypes]
find_multiplicative [lemma, in OAut.ASStructures]
find_pos_begin [lemma, in OAut.Ramsey]
finite [definition, in OAut.NecessityAR]
FiniteClosureIteration [section, in FinTypes.FinTypes]
FiniteClosureIteration.step [variable, in FinTypes.FinTypes]
FiniteClosureIteration.step_dec [variable, in FinTypes.FinTypes]
FiniteClosureIteration.X [variable, in FinTypes.FinTypes]
finiteIndex [definition, in OAut.Ramsey]
FiniteIterationOfString [section, in OAut.Seqs]
FiniteSemiGroup [section, in OAut.Ramsey]
FiniteSemigroup [record, in OAut.Ramsey]
finite_prefix_preserves_infinite [lemma, in OAut.Seqs]
finite_prefix_preserves_infiniteP [lemma, in OAut.Seqs]
FInter [definition, in OAut.AbstractMSO]
finType [record, in FinTypes.FinTypes]
FinType [constructor, in FinTypes.FinTypes]
FinType [library]
finTypeC [record, in FinTypes.FinTypes]
FinTypeC [constructor, in FinTypes.FinTypes]
FinTypeClass2 [instance, in FinTypes.FinTypes]
finTypeC_sub [instance, in FinTypes.FinTypes]
finTypeC_sigT [instance, in FinTypes.FinTypes]
finTypeC_vector [instance, in FinTypes.FinTypes]
finTypeC_sum [instance, in FinTypes.FinTypes]
finTypeC_Option [instance, in FinTypes.FinTypes]
finTypeC_Prod [instance, in FinTypes.FinTypes]
finTypeC_False [instance, in FinTypes.FinTypes]
finTypeC_True [instance, in FinTypes.FinTypes]
finTypeC_empty [instance, in FinTypes.FinTypes]
finTypeC_unit [instance, in FinTypes.FinTypes]
finTypeC_bool [instance, in FinTypes.FinTypes]
finTypeC_Le_K [instance, in OAut.FinType]
finTypeOption_enum [lemma, in FinTypes.FinTypes]
finTypeOption_correct [lemma, in FinTypes.FinTypes]
finTypeProd_enum [lemma, in FinTypes.FinTypes]
FinTypes [library]
finTypeSum_enum [lemma, in FinTypes.FinTypes]
finTypeSum_correct [lemma, in FinTypes.FinTypes]
finType_fromList_correct [lemma, in FinTypes.FinTypes]
finType_fromList [definition, in FinTypes.FinTypes]
finType_sub_enum [lemma, in FinTypes.FinTypes]
finType_sub_correct [lemma, in FinTypes.FinTypes]
finType_sub [definition, in FinTypes.FinTypes]
finType_sigT_enum [lemma, in FinTypes.FinTypes]
finType_sigT_correct [lemma, in FinTypes.FinTypes]
finType_sigT [definition, in FinTypes.FinTypes]
finType_vector_enum [lemma, in FinTypes.FinTypes]
finType_vector_correct [lemma, in FinTypes.FinTypes]
finType_vector [definition, in FinTypes.FinTypes]
finType_sum [definition, in FinTypes.FinTypes]
finType_BoolUnit [definition, in FinTypes.FinTypes]
finType_Prod_correct [lemma, in FinTypes.FinTypes]
finType_Option [definition, in FinTypes.FinTypes]
finType_Prod [definition, in FinTypes.FinTypes]
finType_False [definition, in FinTypes.FinTypes]
finType_True [definition, in FinTypes.FinTypes]
finType_Empty_set [definition, in FinTypes.FinTypes]
finType_bool [definition, in FinTypes.FinTypes]
finType_unit [definition, in FinTypes.FinTypes]
finType_cc [definition, in FinTypes.FinTypes]
finType_exists_dec [instance, in FinTypes.FinTypes]
finType_forall_dec [instance, in FinTypes.FinTypes]
finType_Le_K [definition, in OAut.FinType]
fin_nfa_correct [lemma, in OAut.NecessityAR]
fin_nfa [definition, in OAut.NecessityAR]
fin_iter_last_index [lemma, in OAut.Seqs]
fin_iter_index [lemma, in OAut.Seqs]
fin_iter_to_omega [lemma, in OAut.Seqs]
fin_iter_fin_iter [lemma, in OAut.Seqs]
fin_iter_sum [lemma, in OAut.Seqs]
fin_iter_length_bound [lemma, in OAut.Seqs]
fin_iter_length [lemma, in OAut.Seqs]
fin_iter_split [lemma, in OAut.Seqs]
fin_iter_base [lemma, in OAut.Seqs]
fin_iter_step [lemma, in OAut.Seqs]
fin_iter [definition, in OAut.Seqs]
first [definition, in OAut.BasicDefs]
First [section, in OAut.BasicDefs]
FirstKFinType [section, in OAut.FinType]
first_norm_is_initial [lemma, in OAut.RegularLanguages]
first_order_var_singleton [lemma, in OAut.AbstractMSO]
First.p [variable, in OAut.BasicDefs]
First.p_dec [variable, in OAut.BasicDefs]
Fixedpoints [section, in FinTypes.FinTypes]
Fixedpoints.f [variable, in FinTypes.FinTypes]
Fixedpoints.X [variable, in FinTypes.FinTypes]
fix_first_zero_s_monotone [lemma, in OAut.Seqs]
fix_first_zero [definition, in OAut.Seqs]
Form [inductive, in OAut.AbstractMSO]
FormMin [inductive, in OAut.AbstractMSO]
formulaNFA [definition, in OAut.MSO]
formulaNFA_correct [lemma, in OAut.MSO]
formula_language_complete [lemma, in OAut.MSO]
formula_language [definition, in OAut.MSO]
fp [definition, in FinTypes.FinTypes]
fp_admissible [lemma, in FinTypes.FinTypes]
fp_card_admissible [lemma, in FinTypes.FinTypes]
fp_iter_trans [lemma, in FinTypes.FinTypes]
fp_trans [lemma, in FinTypes.FinTypes]
freeVarInSingleton [lemma, in OAut.AbstractMSO]
free_vars_singleton [lemma, in OAut.AbstractMSO]
free_sings_correct [lemma, in OAut.AbstractMSO]
free_are_sings [abbreviation, in OAut.AbstractMSO]
free_sings [definition, in OAut.AbstractMSO]
free_sings'_correct [lemma, in OAut.AbstractMSO]
free_sings' [definition, in OAut.AbstractMSO]
free_svars [definition, in OAut.AbstractMSO]
free_fvars [definition, in OAut.AbstractMSO]
free_vars_and_incl [lemma, in OAut.AbstractMSO]
free_vars [definition, in OAut.AbstractMSO]
fromFinTypeFromList [definition, in OAut.FinType]
fromListC [instance, in FinTypes.FinTypes]
fromMinMSOInter_fvar [lemma, in OAut.AbstractMSO]
fromMinMSOInter_svar [lemma, in OAut.AbstractMSO]
fromToFVar [lemma, in OAut.AbstractMSO]
fromToSVar [lemma, in OAut.AbstractMSO]
from_ind_nfa_correct [lemma, in OAut.RegularLanguages]
from_ind_nfa [definition, in OAut.RegularLanguages]
from_to_fin_type_from_list [lemma, in OAut.FinType]
fupfate_preserves_singleton [lemma, in OAut.AbstractMSO]
FVar [definition, in OAut.AbstractMSO]
f_weak_coincidence [instance, in OAut.AbstractMSO]

G

getAt [definition, in FinTypes.FinTypes]
getAt_correct [lemma, in FinTypes.FinTypes]
getImage [definition, in FinTypes.FinTypes]
getImage_correct [lemma, in FinTypes.FinTypes]
getImage_length [lemma, in FinTypes.FinTypes]
getImage_in [lemma, in FinTypes.FinTypes]
getPosition [definition, in FinTypes.FinTypes]
getX [definition, in OAut.MSO]
getY [definition, in OAut.MSO]
get_equiv_class_correct [lemma, in OAut.FinType]
get_equiv_class [definition, in OAut.FinType]
get_equiv_class_rep_unique [lemma, in OAut.FinType]
get_equiv_class_rep_less [lemma, in OAut.FinType]
get_equiv_class_rep_equiv [lemma, in OAut.FinType]
get_equiv_class_rep [definition, in OAut.FinType]
ge_to_le [lemma, in OAut.Seqs]

H

has_monochromatic_subsequence [definition, in OAut.Ramsey]
Hedberg [lemma, in FinTypes.BasicDefinitions]
HelpApply [lemma, in FinTypes.FinTypes]
holdsIn [definition, in OAut.Seqs]

I

idempotent [definition, in OAut.Ramsey]
idempotent_mul [lemma, in OAut.Ramsey]
id_Le_K [definition, in OAut.FinType]
iff_dec [instance, in FinTypes.External]
image [definition, in FinTypes.FinTypes]
Image [definition, in OAut.Seqs]
ImageNFA [section, in OAut.Buechi]
ImageNFA.aut [variable, in OAut.Buechi]
ImageNFA.f [variable, in OAut.Buechi]
images [definition, in FinTypes.FinTypes]
imagesDupfree [lemma, in FinTypes.FinTypes]
imagesInnerLength [lemma, in FinTypes.FinTypes]
imagesNonempty [lemma, in FinTypes.FinTypes]
images_length [lemma, in FinTypes.FinTypes]
image_aut_correct [lemma, in OAut.Buechi]
image_accepts_aut [lemma, in OAut.Buechi]
image_aut [definition, in OAut.Buechi]
image_transition [definition, in OAut.Buechi]
impl_dec [instance, in FinTypes.External]
impl_correct [lemma, in OAut.AbstractMSO]
Incl [constructor, in OAut.AbstractMSO]
inclp [definition, in FinTypes.External]
Inclusion [section, in FinTypes.External]
Inclusion.X [variable, in FinTypes.External]
incl_equi_proper [instance, in FinTypes.External]
incl_preorder [instance, in FinTypes.External]
incl_app_left [lemma, in FinTypes.External]
incl_lrcons [lemma, in FinTypes.External]
incl_rcons [lemma, in FinTypes.External]
incl_sing [lemma, in FinTypes.External]
incl_lcons [lemma, in FinTypes.External]
incl_shift [lemma, in FinTypes.External]
incl_nil_eq [lemma, in FinTypes.External]
incl_map [lemma, in FinTypes.External]
incl_nil [lemma, in FinTypes.External]
incl_nfa_correct [lemma, in OAut.MSO]
incl_implies_accepting [lemma, in OAut.MSO]
incl_nfa [definition, in OAut.MSO]
incl_transition [definition, in OAut.MSO]
incl_state [definition, in OAut.MSO]
inConcatCons [lemma, in FinTypes.FinTypes]
InCount [lemma, in FinTypes.BasicDefinitions]
index [definition, in FinTypes.FinTypes]
ind_dfa_to_nfa_correct [lemma, in OAut.RegularLanguages]
ind_nfa_to_dfa_correct [lemma, in OAut.RegularLanguages]
infinite [abbreviation, in OAut.Seqs]
infinite [abbreviation, in OAut.Seqs]
Infinite [section, in OAut.Seqs]
InfiniteConcat [section, in OAut.Seqs]
InfiniteFilter [section, in OAut.Seqs]
InfiniteFilter.infP [variable, in OAut.Seqs]
InfiniteFilter.P [variable, in OAut.Seqs]
InfiniteFilter.w [variable, in OAut.Seqs]
infiniteP [definition, in OAut.Seqs]
InfinitePigeonholePrinciple [definition, in OAut.Ramsey]
infiniteP_proper [instance, in OAut.Seqs]
infinite_equiv_indices_dm [lemma, in OAut.NecessityAR]
infinite_final_strings_R [lemma, in OAut.Complement]
infinite_filter_zero [lemma, in OAut.Seqs]
infinite_filter_all [lemma, in OAut.Seqs]
infinite_filter_correct [lemma, in OAut.Seqs]
infinite_filter_s_monotone [lemma, in OAut.Seqs]
infinite_filter [definition, in OAut.Seqs]
infinite_final_implies_infinite_critical [lemma, in OAut.ASStructures]
infinite_merge_at_next_same_color [lemma, in OAut.Ramsey]
infinite_merge_at_next [lemma, in OAut.Ramsey]
infinite_equiv_indices' [lemma, in OAut.Ramsey]
inImages [lemma, in FinTypes.FinTypes]
initial [definition, in OAut.Buechi]
initialW_partitions_in_W [lemma, in OAut.Buechi]
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 FinTypes.BasicDefinitions]
injectiveApply [lemma, in FinTypes.BasicDefinitions]
injective_dupfree [lemma, in FinTypes.FinTypes]
inr_fix [lemma, in FinTypes.Automata]
inr_fix_epsilon [lemma, in FinTypes.Automata]
intermediate_infinite [lemma, in OAut.NecessityAR]
intersect [definition, in FinTypes.Automata]
intersect [definition, in OAut.Buechi]
IntersectionClosure [section, in OAut.Buechi]
IntersectionClosure.aut_2 [variable, in OAut.Buechi]
IntersectionClosure.aut_1 [variable, in OAut.Buechi]
IntersectionClosure.IRun [section, in OAut.Buechi]
IntersectionClosure.IRun.F1 [variable, in OAut.Buechi]
IntersectionClosure.IRun.F2 [variable, in OAut.Buechi]
IntersectionClosure.IRun.r_2 [variable, in OAut.Buechi]
IntersectionClosure.IRun.r_1 [variable, in OAut.Buechi]
IntersectionClosure.IRun.w [variable, in OAut.Buechi]
intersection_incl_intersect [lemma, in OAut.Buechi]
intersection_transition [definition, in OAut.Buechi]
intersection_final [definition, in OAut.Buechi]
intersection_initial [definition, in OAut.Buechi]
intersection_state [definition, in OAut.Buechi]
intersect_correct [lemma, in FinTypes.Automata]
intersect_correct [lemma, in OAut.Buechi]
intersect_incl_aut2 [lemma, in OAut.Buechi]
intersect_incl_aut1 [lemma, in OAut.Buechi]
intersect_acorrect [lemma, in OAut.ASStructures]
interToSeq [definition, in OAut.MSO]
inter_to_seq_to_inter_correct [lemma, in OAut.MSO]
inv_join_separate [lemma, in OAut.FinType]
inv_separate_join [lemma, in OAut.FinType]
inv_nat_to_pair [lemma, in OAut.Ramsey]
in_rem_iff [lemma, in FinTypes.External]
in_filter_iff [lemma, in FinTypes.External]
in_equi_proper [instance, in FinTypes.External]
in_incl_proper [instance, in FinTypes.External]
in_cons_neq [lemma, in FinTypes.External]
in_sing [lemma, in FinTypes.External]
in_vP_correct [lemma, in OAut.NecessityAR]
in_vP [definition, in OAut.NecessityAR]
in_undup [lemma, in FinTypes.FinTypes]
in_lang [abbreviation, in FinTypes.Automata]
in_lang [abbreviation, in FinTypes.Automata]
in_lang_prepend [lemma, in OAut.Seqs]
in_equiv_class [definition, in OAut.FinType]
ipp [lemma, in OAut.Ramsey]
ipp_dm [lemma, in OAut.NecessityAR]
irun [definition, in OAut.Buechi]
irun_final [lemma, in OAut.Buechi]
irun_step_final [lemma, in OAut.Buechi]
irun_same_states [lemma, in OAut.Buechi]
irun_step_to_true [lemma, in OAut.Buechi]
irun_initial [lemma, in OAut.Buechi]
irun_valid [lemma, in OAut.Buechi]
IsSucc [definition, in OAut.AbstractMSO]
isSuccCorrect [lemma, in OAut.AbstractMSO]
IsSuccMem [definition, in OAut.AbstractMSO]
isSuccMemCorrect [lemma, in OAut.AbstractMSO]
is_ramseyan_factorization [definition, in OAut.Ramsey]
ItoM0 [definition, in OAut.AbstractMSO]
ItoM0Fvar [lemma, in OAut.AbstractMSO]
ItoM0Svar [lemma, in OAut.AbstractMSO]
ItoM1 [definition, in OAut.AbstractMSO]
ItoM2 [definition, in OAut.AbstractMSO]
ItoM2_fvar_update [lemma, in OAut.AbstractMSO]
I2chain [definition, in OAut.MSO]

J

join [definition, in OAut.FinType]
joinASeq [definition, in OAut.MSO]
joinASeq_correct_old [lemma, in OAut.MSO]
joinASeq_correct_new [lemma, in OAut.MSO]
join_snd [lemma, in OAut.FinType]
join_fst [lemma, in OAut.FinType]

K

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

L

LAmap [definition, in OAut.ASStructures]
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]
LanguageOmegaIteration [section, in OAut.Seqs]
LanguageOmegaIteration.l [variable, in OAut.Seqs]
Languages [section, in OAut.BasicDefs]
Languages.X [variable, in OAut.BasicDefs]
language_complement_proper [instance, in OAut.BasicDefs]
language_difference_proper [instance, in OAut.BasicDefs]
language_intersection_proper [instance, in OAut.BasicDefs]
language_union_proper [instance, in OAut.BasicDefs]
language_eq_mem [instance, in OAut.BasicDefs]
language_eq_equivalence [instance, 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 FinTypes.Automata]
lang_equiv [definition, in FinTypes.Automata]
lang_incl_iff [lemma, in FinTypes.Automata]
lang_incl [definition, in FinTypes.Automata]
lang_prepend_proper [instance, in OAut.Seqs]
lang_prepend [definition, in OAut.Seqs]
lang_omega_iteration_proper [instance, in OAut.Seqs]
lang_omega_iteration_extensional [lemma, in OAut.Seqs]
lang_o_iter_extract [lemma, in OAut.Seqs]
lang_o_iter [definition, in OAut.Seqs]
LAproj_list [definition, in OAut.MSO]
lastindex [projection, in OAut.Seqs]
last_norm_is_final [lemma, in OAut.RegularLanguages]
LA_proj_list_equiv_image [lemma, in OAut.MSO]
Le [constructor, in OAut.AbstractMSO]
least_fp_containing [definition, in FinTypes.FinTypes]
len [abbreviation, in OAut.NFAs]
lengthEq [lemma, in FinTypes.BasicDefinitions]
Leq [definition, in OAut.AbstractMSO]
leq_correct [lemma, in OAut.AbstractMSO]
leq_0 [lemma, in OAut.Complement]
less_nfa_correct [lemma, in OAut.MSO]
less_implies_accepting [lemma, in OAut.MSO]
less_nfa [definition, in OAut.MSO]
less_transition [definition, in OAut.MSO]
less_state [definition, in OAut.MSO]
le_correct [lemma, in OAut.AbstractMSO]
le_add [lemma, in OAut.Seqs]
le_L_is_le [lemma, in OAut.FinType]
Le_K_enum_ok [lemma, in OAut.FinType]
LE_K_eq_dec [instance, in OAut.FinType]
Le_K [definition, in OAut.FinType]
le_k [definition, in OAut.FinType]
ListProjection [section, in OAut.MSO]
list_cc [lemma, in FinTypes.External]
list_exists_not_incl [lemma, in FinTypes.External]
list_exists_DM [lemma, in FinTypes.External]
list_exists_dec [instance, in FinTypes.External]
list_forall_dec [instance, in FinTypes.External]
list_sigma_forall [lemma, in FinTypes.External]
list_cycle [lemma, in FinTypes.External]
list_in_dec [instance, in FinTypes.External]
list_eq_dec [instance, in FinTypes.External]
list_are_sings [abbreviation, in OAut.AbstractMSO]
list_proj_aut [definition, in OAut.MSO]
list_eq [lemma, in OAut.FinType]
logic_dec_satis [instance, in OAut.NecessityAR]
logic_dec [definition, in OAut.BasicDefs]
loop [lemma, in FinTypes.BasicDefinitions]
loop [projection, in OAut.Seqs]
loop_admits_ramseyan_fac [lemma, in OAut.Ramsey]
loop'b [abbreviation, in OAut.Seqs]
L_dind [definition, in OAut.RegularLanguages]
L_ind [definition, in OAut.RegularLanguages]
L_A [definition, in OAut.ASStructures]

M

MAnd [constructor, in OAut.AbstractMSO]
map_aut_up_correct [lemma, in OAut.ASStructures]
map_aut_acorrect [projection, in OAut.ASStructures]
Markov [definition, in OAut.Ramsey]
max_le [lemma, in OAut.BasicDefs]
max_le_right [lemma, in OAut.BasicDefs]
max_le_left [lemma, in OAut.BasicDefs]
max_of_nat_string_correct [lemma, in OAut.Ramsey]
max_of_nat_string [definition, in OAut.Ramsey]
mC [definition, in FinTypes.FinTypes]
Mem [constructor, in OAut.AbstractMSO]
Membership [section, in FinTypes.External]
Membership.X [variable, in FinTypes.External]
memSet [projection, in OAut.AbstractMSO]
memSet_proper [instance, in OAut.AbstractMSO]
memX [definition, in OAut.MSO]
MEx [constructor, in OAut.AbstractMSO]
MIncl [constructor, in OAut.AbstractMSO]
minmso_classic [lemma, in OAut.MSO]
minsat [definition, in OAut.AbstractMSO]
minsat_iff_buechi_non_empty [lemma, in OAut.MSO]
mkAdmissibleSequenceStructure [constructor, in OAut.ASStructures]
mkNatSet [constructor, in OAut.AbstractMSO]
mknfa [constructor, in OAut.NFAs]
mkSequenceStructure [constructor, in OAut.ASStructures]
mkSG [constructor, in OAut.Ramsey]
mkstring [constructor, in OAut.Seqs]
mkUPSeq [constructor, in OAut.Seqs]
MLe [constructor, in OAut.AbstractMSO]
mmC [definition, in FinTypes.FinTypes]
MNeg [constructor, in OAut.AbstractMSO]
MNotEmpty [definition, in OAut.AbstractMSO]
msatisfies [definition, in OAut.AbstractMSO]
msatisfies_set_extensional [lemma, in OAut.AbstractMSO]
msatisfies_extensional [lemma, in OAut.AbstractMSO]
MSingleton [definition, in OAut.AbstractMSO]
MSO [section, in OAut.AbstractMSO]
MSO [library]
MSOClassicalImpliesRamseyFac [section, in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.ADD_Formula.vP [variable, in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.ADD_Formula.vX [variable, in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.ADD_Formula [section, in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.f [variable, in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.MSO_XM [variable, in OAut.NecessityAR]
_ ~~# _ [notation, in OAut.NecessityAR]
_ ~~@ _ at _ [notation, in OAut.NecessityAR]
MSOtoBuechi [section, in OAut.MSO]
MSOtoBuechi.BaseNFAs [section, in OAut.MSO]
MSOtoBuechi.BaseNFAs.InclusionNFA [section, in OAut.MSO]
InclS [notation, in OAut.MSO]
NotInclS [notation, in OAut.MSO]
MSOtoBuechi.BaseNFAs.LessNFA [section, in OAut.MSO]
Less [notation, in OAut.MSO]
SearchX [notation, in OAut.MSO]
SearchY [notation, in OAut.MSO]
MSOtoBuechi.BaseNFAs.X [variable, in OAut.MSO]
MSOtoBuechi.BaseNFAs.Y [variable, in OAut.MSO]
A [notation, in OAut.MSO]
L_M [notation, in OAut.MSO]
mso_xm_implies_ramsey_fac [lemma, in OAut.NecessityAR]
mso_ramseyan_factorization [lemma, in OAut.NecessityAR]
MSO_Classical [definition, in OAut.NecessityAR]
mso_DM_exist_neg' [lemma, in OAut.AbstractMSO]
mso_DM_exist_neg [lemma, in OAut.AbstractMSO]
mso_DM_forall_neg' [lemma, in OAut.AbstractMSO]
mso_DM_forall_neg [lemma, in OAut.AbstractMSO]
mso_DM_ex2 [lemma, in OAut.AbstractMSO]
mso_DM_ex1 [lemma, in OAut.AbstractMSO]
mso_DM_finBigAND' [lemma, in OAut.AbstractMSO]
mso_DM_finBigAND [lemma, in OAut.AbstractMSO]
mso_DM_finBigOR' [lemma, in OAut.AbstractMSO]
mso_DM_finBigOR [lemma, in OAut.AbstractMSO]
mso_DM_impl [lemma, in OAut.AbstractMSO]
mso_DM_neg_and' [lemma, in OAut.AbstractMSO]
mso_DM_neg_and [lemma, in OAut.AbstractMSO]
mso_DM_neg_or [lemma, in OAut.AbstractMSO]
mso_DN [lemma, in OAut.AbstractMSO]
mso_impl [definition, in OAut.AbstractMSO]
mso_xm_satisfies [lemma, in OAut.AbstractMSO]
mso_coincidence_bi [lemma, in OAut.AbstractMSO]
mso_coincidence' [lemma, in OAut.AbstractMSO]
mso_coincidence [lemma, in OAut.AbstractMSO]
mso_equiv [definition, in OAut.AbstractMSO]
mso_classic [lemma, in OAut.MSO]
MSO.ReducablityOfFirstOrderVariables [section, in OAut.AbstractMSO]
<< _ , _ >> [notation, in OAut.AbstractMSO]
<\ _ |> [notation, in OAut.AbstractMSO]
<| _ /> [notation, in OAut.AbstractMSO]
[ _ ] [notation, in OAut.AbstractMSO]
MSO.SyntacticSugarFirstOrder [section, in OAut.AbstractMSO]
_ =~~= _ [notation, in OAut.AbstractMSO]
_ # _ |== _ [notation, in OAut.AbstractMSO]
_ |= _ [notation, in OAut.AbstractMSO]
mul [definition, in OAut.Ramsey]
mul_div [lemma, in OAut.BasicDefs]
mul_geq_left [lemma, in OAut.BasicDefs]
mul_ge_0_reverse [lemma, in OAut.BasicDefs]
mul_ge_0 [lemma, in OAut.BasicDefs]
mul_yields_idempotent [lemma, in OAut.Ramsey]
mul_mult [lemma, in OAut.Ramsey]
mul_distr [lemma, in OAut.Ramsey]
mul_comm [lemma, in OAut.Ramsey]
mul_step [lemma, in OAut.Ramsey]
MyhillNerode [definition, in OAut.Complement]

N

narrowASeq [definition, in OAut.MSO]
narrowVector [definition, in OAut.FinType]
narrowVectorCorrect [lemma, in OAut.FinType]
narrow_to_free_vars [lemma, in OAut.MSO]
NatCover [definition, in OAut.MSO]
NatPartition [definition, in OAut.MSO]
NatSet [projection, in OAut.AbstractMSO]
NatSetClass [record, in OAut.AbstractMSO]
NatSetFromSeq [instance, in OAut.MSO]
NatUnique [definition, in OAut.MSO]
nat_le_dec [instance, in FinTypes.External]
nat_eq_dec [instance, in FinTypes.External]
nat_partition_extensional [lemma, in OAut.MSO]
nat_equation_1 [lemma, in OAut.Seqs]
nat_pair_le_not_equal [lemma, in OAut.Seqs]
nat_pair_le [definition, in OAut.Seqs]
nat_to_pair_halfspace [lemma, in OAut.Ramsey]
nat_to_pair [definition, in OAut.Ramsey]
NecessityAR [library]
Neg [constructor, in OAut.AbstractMSO]
negOr [lemma, in FinTypes.BasicDefinitions]
neg_F [definition, in FinTypes.Automata]
next_position_exists_all [lemma, in OAut.Seqs]
next_position_exists_correct [lemma, in OAut.Seqs]
next_position_exists_increasing [lemma, in OAut.Seqs]
next_position_exists [definition, in OAut.Seqs]
next_position_all [lemma, in OAut.Seqs]
next_position_bounds [lemma, in OAut.Seqs]
next_position_correct [lemma, in OAut.Seqs]
next_position [definition, in OAut.Seqs]
NFA [record, in OAut.NFAs]
nfa [record, in FinTypes.Automata]
NFA [constructor, in FinTypes.Automata]
NFAOmegaIteration [section, in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized [section, in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized.aut [variable, in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized.finalW [variable, in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized.initialW [variable, in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized.normW [variable, in OAut.Buechi]
NFAs [library]
NFAStringLanguage [section, in OAut.RegularLanguages]
nfa_string_lang_cc [lemma, in OAut.RegularLanguages]
nfa_omega_iter_correct [lemma, in OAut.Buechi]
nfa_omega_iter [definition, in OAut.Buechi]
nfa_omega_iter'_correct [lemma, in OAut.Buechi]
nfa_omega_iter'_accepts_aut [lemma, in OAut.Buechi]
nfa_omega_iter' [definition, in OAut.Buechi]
nil_kleene [lemma, in FinTypes.Automata]
NoneElement [lemma, in FinTypes.FinTypes]
normalize [definition, in OAut.RegularLanguages]
NormalizeNFA [section, in OAut.RegularLanguages]
NormalizeNFA.aut [variable, in OAut.RegularLanguages]
Final [notation, in OAut.RegularLanguages]
Initial [notation, in OAut.RegularLanguages]
normalize_is_normalized [lemma, in OAut.RegularLanguages]
normalize_final [definition, in OAut.RegularLanguages]
normalize_inital [definition, in OAut.RegularLanguages]
normalize_correct [lemma, in OAut.RegularLanguages]
normalize_accepts_aut [lemma, in OAut.RegularLanguages]
norm_transition [definition, in OAut.RegularLanguages]
norm_final_state [definition, in OAut.RegularLanguages]
norm_initial_state [definition, in OAut.RegularLanguages]
norm_state [definition, in OAut.RegularLanguages]
notInMapCons [lemma, in FinTypes.FinTypes]
notInZero [lemma, in FinTypes.BasicDefinitions]
not_in_cons [lemma, in FinTypes.External]
not_dec [instance, in FinTypes.External]
not_finite_implies_infinite [lemma, in OAut.NecessityAR]
not_finite_intermediate [lemma, in OAut.NecessityAR]
not_empty_correct [lemma, in OAut.AbstractMSO]
not_part_of_complement_implies_aut [lemma, in OAut.ASStructures]
not_tilde_w_equiv_sym [lemma, in OAut.Ramsey]
no_a [abbreviation, in OAut.NecessityAR]
NullMul [lemma, in FinTypes.BasicDefinitions]
nums_leq_K_length [lemma, in OAut.FinType]
nums_leq_K_dupfree [lemma, in OAut.FinType]
nums_leq_K_complete [lemma, in OAut.FinType]
nums_leq_K [definition, in OAut.FinType]
n_accept [definition, in FinTypes.Automata]

O

oiter_transition [definition, in OAut.Buechi]
OmegaIteration [section, in OAut.Seqs]
OmegaNatSet [instance, in OAut.NecessityAR]
OmegaSequenceStructure [definition, in OAut.ASStructures]
OmegaStructure [definition, in OAut.ASStructures]
omega_iteration_final [lemma, in OAut.Buechi]
omega_classic [instance, in OAut.MSO]
omega_sat [abbreviation, in OAut.MSO]
omega_iteration_infiniteP [lemma, in OAut.Seqs]
omega_iter_unfold [lemma, in OAut.Seqs]
omega_iter_first_new [lemma, in OAut.Seqs]
omega_iter_first [lemma, in OAut.Seqs]
omega_iteration_proper_index [instance, in OAut.Seqs]
omega_iteration_proper [instance, in OAut.Seqs]
omega_iteration_extensional [lemma, in OAut.Seqs]
omega_iteration [definition, in OAut.Seqs]
omega_iteration_valid_run [lemma, in OAut.ASStructures]
onestate [definition, in FinTypes.Automata]
onestate_correct [lemma, in FinTypes.Automata]
OneStringNFA [section, in OAut.RegularLanguages]
OneStringNFA.v [variable, in OAut.RegularLanguages]
Option_Card [lemma, in FinTypes.FinTypes]
option_enum_ok [lemma, in FinTypes.FinTypes]
option_eq_dec [instance, in FinTypes.BasicDefinitions]
Or [definition, in OAut.AbstractMSO]
or_dec [instance, in FinTypes.External]
or_correct [lemma, in OAut.AbstractMSO]
os_nfa_correct [lemma, in OAut.RegularLanguages]
os_nfa_only_accepts_v [lemma, in OAut.RegularLanguages]
os_nfa_accepts_v [lemma, in OAut.RegularLanguages]
os_accepting_run [definition, in OAut.RegularLanguages]
os_nfa [definition, in OAut.RegularLanguages]
os_transition [definition, in OAut.RegularLanguages]
os_final [definition, in OAut.RegularLanguages]
os_initial [definition, in OAut.RegularLanguages]
os_state [definition, in OAut.RegularLanguages]
other_norm_is_aut_state [lemma, in OAut.RegularLanguages]

P

Pairs [definition, in OAut.Ramsey]
pair_proj2 [lemma, in OAut.BasicDefs]
pair_proj1 [lemma, in OAut.BasicDefs]
pair_nat_choice [lemma, in OAut.Ramsey]
pair_to_nat [definition, in OAut.Ramsey]
Partition [definition, in OAut.MSO]
Partition [section, in OAut.MSO]
partition_run_on_concat_inf [lemma, in OAut.Buechi]
partition_run_on_prepend_string [lemma, in OAut.Buechi]
partition_correct [lemma, in OAut.MSO]
part_of_complement_implies_complement [lemma, in OAut.ASStructures]
path [definition, in OAut.NFAs]
PathTriple [abbreviation, in OAut.NFAs]
path_length_bounded [lemma, in OAut.NFAs]
path_proper [instance, in OAut.NFAs]
path_extensional [lemma, in OAut.NFAs]
periodic_run_matching_pseq_size [lemma, in OAut.ASStructures]
periodic_run [lemma, in OAut.ASStructures]
pick [lemma, in FinTypes.FinTypes]
pickx [definition, in FinTypes.FinTypes]
pidgeonHole_bij [lemma, in FinTypes.FinTypes]
pidgeonHole_surj [lemma, in FinTypes.FinTypes]
pidgeonHole_inj [lemma, in FinTypes.FinTypes]
power [definition, in FinTypes.External]
PowerRep [section, in FinTypes.External]
PowerRep.X [variable, in FinTypes.External]
power_extensional [lemma, in FinTypes.External]
power_nil [lemma, in FinTypes.External]
power_incl [lemma, in FinTypes.External]
pow_ge_zero [lemma, in OAut.BasicDefs]
pow_ge_zero' [lemma, in OAut.BasicDefs]
predCons [definition, in FinTypes.Automata]
predCons_dec [instance, in FinTypes.Automata]
predicate [projection, in FinTypes.External]
prefix [projection, in OAut.Seqs]
prefix_admits_ramseyan_fac [lemma, in OAut.Ramsey]
PreImage [definition, in OAut.Seqs]
PreImageNFA [section, in OAut.Buechi]
PreImageNFA.aut [variable, in OAut.Buechi]
PreImageNFA.f [variable, in OAut.Buechi]
preimage_aut_correct [lemma, in OAut.Buechi]
preimage_aut [definition, in OAut.Buechi]
preimage_aut_acorrect [lemma, in OAut.ASStructures]
prepend [definition, in OAut.Seqs]
PrependNFA [section, in OAut.Buechi]
PrependNFA.PrependNormalizedNFA [section, in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.aut_2 [variable, in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.aut_1 [variable, in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.finalV [variable, in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.initialV [variable, in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.norm [variable, in OAut.Buechi]
prepend_step_valid_path [lemma, in OAut.NFAs]
prepend_nfa_correct [lemma, in OAut.Buechi]
prepend_nfa [definition, in OAut.Buechi]
prepend_nfa'_correct [lemma, in OAut.Buechi]
prepend_aut_accepts_prepend_omega [lemma, in OAut.Buechi]
prepend_aut_is_prepend_omega [lemma, in OAut.Buechi]
prepend_nfa' [definition, in OAut.Buechi]
prepend_state_initial [definition, in OAut.Buechi]
prepend_state_final [definition, in OAut.Buechi]
prepend_transition [definition, in OAut.Buechi]
prepend_state [definition, in OAut.Buechi]
prepend_on_omega_iteration [lemma, in OAut.Seqs]
prepend_string_proper_index [instance, in OAut.Seqs]
prepend_string_proper [instance, in OAut.Seqs]
prepend_string_rest'' [lemma, in OAut.Seqs]
prepend_string_rest' [lemma, in OAut.Seqs]
prepend_string_rest [lemma, in OAut.Seqs]
prepend_string_begin [lemma, in OAut.Seqs]
prepend_string [definition, in OAut.Seqs]
prepend_prefix_begin [lemma, in OAut.Seqs]
prepend_prefix_rest' [lemma, in OAut.Seqs]
prepend_prefix_rest2 [lemma, in OAut.Seqs]
prepend_prefix_rest [lemma, in OAut.Seqs]
prepend_rest2 [lemma, in OAut.Seqs]
prepend_rest [lemma, in OAut.Seqs]
prepend_first [lemma, in OAut.Seqs]
prepend_prefix [definition, in OAut.Seqs]
prepend_string_valid_run [lemma, in OAut.ASStructures]
preservation_FCIter [lemma, in FinTypes.FinTypes]
preservation_iter [lemma, in FinTypes.FinTypes]
preservation_step [lemma, in FinTypes.FinTypes]
prod [definition, in FinTypes.Automata]
ProdCount [lemma, in FinTypes.FinTypes]
prodLists [definition, in FinTypes.BasicDefinitions]
Prod_Card [lemma, in FinTypes.FinTypes]
prod_enum_ok [lemma, in FinTypes.FinTypes]
prod_correct [lemma, in FinTypes.Automata]
prod_delta_star [lemma, in FinTypes.Automata]
prod_F [definition, in FinTypes.Automata]
prod_pred_dec [instance, in FinTypes.Automata]
prod_pred [definition, in FinTypes.Automata]
prod_delta [definition, in FinTypes.Automata]
prod_nil [lemma, in FinTypes.BasicDefinitions]
prod_eq_dec [instance, in FinTypes.BasicDefinitions]
projection_list_aclosed [lemma, in OAut.MSO]
proj1_sig_fun [lemma, in FinTypes.BasicDefinitions]
proveOne [lemma, in FinTypes.FinTypes]
pure [definition, in FinTypes.BasicDefinitions]
pure_eq [lemma, in FinTypes.BasicDefinitions]
pure_impure [lemma, in FinTypes.BasicDefinitions]
pure_equiv [lemma, in FinTypes.BasicDefinitions]
pure_W_final [definition, in OAut.Complement]
pure_le_k_iff [lemma, in OAut.FinType]
purify [lemma, in FinTypes.BasicDefinitions]

Q

Q [projection, in FinTypes.Automata]
Quotients [section, in OAut.FinType]
Quotients.E [variable, in OAut.FinType]
Quotients.EisEquiv [variable, in OAut.FinType]
Q_acc [projection, in FinTypes.Automata]
q0 [projection, in FinTypes.Automata]

R

Ramsey [library]
RamseyanFactorizationMarkov [section, in OAut.Ramsey]
ramseyan_factorization [lemma, in OAut.Ramsey]
RamseyFac [definition, in OAut.Ramsey]
RamseyFacFromComplement [lemma, in OAut.NecessityAR]
RamseyFacImpliesMarkov [lemma, in OAut.Ramsey]
RamseyFac_iff_AdditiveRamsey [lemma, in OAut.Ramsey]
ramseyTotality [lemma, in OAut.Complement]
ramsey_nfa_correct [lemma, in OAut.NecessityAR]
ramsey_nfa [definition, in OAut.NecessityAR]
ramsey_idem_aut_correct [lemma, in OAut.NecessityAR]
ramsey_idem_aut [definition, in OAut.NecessityAR]
ramsey_idem_aut'_scorrect [lemma, in OAut.NecessityAR]
ramsey_idem_aut'_run_is_inl [lemma, in OAut.NecessityAR]
ramsey_idem_aut'_run [definition, in OAut.NecessityAR]
ramsey_idem_aut' [definition, in OAut.NecessityAR]
ramsey_transition [definition, in OAut.NecessityAR]
ramsey_state [abbreviation, in OAut.NecessityAR]
reach [definition, in FinTypes.Automata]
reachable [definition, in OAut.NFAs]
reachable [inductive, in FinTypes.Automata]
reachable_with_something_dec [instance, in FinTypes.Automata]
reachable_dec [instance, in FinTypes.Automata]
reachable_transitive [lemma, in FinTypes.Automata]
reachable_with_reachable [lemma, in FinTypes.Automata]
reachable_with [definition, in FinTypes.Automata]
reach_reachable_with [lemma, in FinTypes.Automata]
reach_correct [lemma, in FinTypes.Automata]
reach_correct2 [lemma, in FinTypes.Automata]
reach_correct2' [lemma, in FinTypes.Automata]
reach_correct1 [lemma, in FinTypes.Automata]
reach_least_fp [lemma, in FinTypes.Automata]
refines [definition, in OAut.Complement]
refl [constructor, in FinTypes.Automata]
RegularLanguages [library]
relation [projection, in FinTypes.External]
rem [definition, in FinTypes.External]
Removal [section, in FinTypes.External]
Removal.X [variable, in FinTypes.External]
rem_inclr [lemma, in FinTypes.External]
rem_reorder [lemma, in FinTypes.External]
rem_id [lemma, in FinTypes.External]
rem_fst' [lemma, in FinTypes.External]
rem_fst [lemma, in FinTypes.External]
rem_comm [lemma, in FinTypes.External]
rem_equi [lemma, in FinTypes.External]
rem_app' [lemma, in FinTypes.External]
rem_app [lemma, in FinTypes.External]
rem_neq [lemma, in FinTypes.External]
rem_in [lemma, in FinTypes.External]
rem_cons' [lemma, in FinTypes.External]
rem_cons [lemma, in FinTypes.External]
rem_mono [lemma, in FinTypes.External]
rem_incl [lemma, in FinTypes.External]
rem_not_in [lemma, in FinTypes.External]
rem_loops_preserves_ends [lemma, in OAut.NFAs]
rem_loops'_preserves_ends [lemma, in OAut.NFAs]
rem_loops_length [lemma, in OAut.NFAs]
rem_loops'_length [lemma, in OAut.NFAs]
rem_loops_valid [lemma, in OAut.NFAs]
rem_loops'_valid [lemma, in OAut.NFAs]
rem_loops [definition, in OAut.NFAs]
rem_loops' [definition, in OAut.NFAs]
rem_not_in_eq [lemma, in OAut.FinType]
rem_sub [lemma, in OAut.FinType]
rep [definition, in FinTypes.External]
rep_dupfree [lemma, in FinTypes.External]
rep_idempotent [lemma, in FinTypes.External]
rep_injective [lemma, in FinTypes.External]
rep_eq [lemma, in FinTypes.External]
rep_eq' [lemma, in FinTypes.External]
rep_mono [lemma, in FinTypes.External]
rep_equi [lemma, in FinTypes.External]
rep_in [lemma, in FinTypes.External]
rep_incl [lemma, in FinTypes.External]
rep_power [lemma, in FinTypes.External]
rest [definition, in OAut.FinType]
revert_concat_second [lemma, in OAut.Seqs]
revert_concat_first [lemma, in OAut.Seqs]
revert_drop [lemma, in OAut.Seqs]
revert_prepend_string [lemma, in OAut.Seqs]
rightResult [lemma, in FinTypes.FinTypes]
right_congruent [definition, in OAut.Complement]
run [abbreviation, in OAut.NFAs]
Run [definition, in OAut.NFAs]
run_for_transforms_correct [lemma, in OAut.Complement]
run_for_transforms [definition, in OAut.Complement]
r' [definition, in OAut.Complement]
R' [definition, in OAut.Complement]
R'k0_eq_Rk0 [lemma, in OAut.Complement]

S

s [projection, in FinTypes.Automata]
S [projection, in FinTypes.Automata]
saccepting [definition, in OAut.RegularLanguages]
safe [inductive, in OAut.BasicDefs]
safeB [constructor, in OAut.BasicDefs]
safeS [constructor, in OAut.BasicDefs]
safe_dclosed [lemma, in OAut.BasicDefs]
SAll [definition, in OAut.AbstractMSO]
sat [definition, in OAut.AbstractMSO]
satisfies [definition, in OAut.AbstractMSO]
sat_iff_minsat [lemma, in OAut.AbstractMSO]
sat_fromMinMSO_s_update [lemma, in OAut.AbstractMSO]
sat_fromMinMSO_update [lemma, in OAut.AbstractMSO]
sat_fromMinMSO [lemma, in OAut.AbstractMSO]
sat_iff_buechi_non_empty [lemma, in OAut.MSO]
sautomaton_normalized [definition, in OAut.RegularLanguages]
sclosure_complement [lemma, in OAut.RegularLanguages]
sclosure_diff [lemma, in OAut.RegularLanguages]
sclosure_intersection [lemma, in OAut.RegularLanguages]
sclosure_union [lemma, in OAut.RegularLanguages]
scomplement [definition, in OAut.RegularLanguages]
scomplement_correct [lemma, in OAut.RegularLanguages]
sdiff [definition, in OAut.RegularLanguages]
sdiff_correct [lemma, in OAut.RegularLanguages]
seaccepting [definition, in OAut.Complement]
second_order_interpretation [lemma, in OAut.AbstractMSO]
second_order_var_singleton [lemma, in OAut.AbstractMSO]
selanguage [definition, in OAut.Complement]
selectX [definition, in OAut.MSO]
separate [definition, in OAut.FinType]
separate_unchanged [lemma, in OAut.FinType]
seq [projection, in OAut.Seqs]
Seq [definition, in OAut.Seqs]
SeqLang [abbreviation, in OAut.Seqs]
SeqLang_Extensional [definition, in OAut.Seqs]
SeqOperations [section, in OAut.Seqs]
Seqs [library]
seqToInter [definition, in OAut.MSO]
seqToInterGetX [lemma, in OAut.MSO]
seqToInterGetY [lemma, in OAut.MSO]
seqToList [definition, in OAut.RegularLanguages]
seqToSet [definition, in OAut.MSO]
seqToSetCorrect [lemma, in OAut.MSO]
seqToSetCover [lemma, in OAut.MSO]
seqToSetPartition [lemma, in OAut.MSO]
seqToSetUnique [lemma, in OAut.MSO]
SequenceStructure [record, in OAut.ASStructures]
seq_to_sets [definition, in OAut.NecessityAR]
seq_implies_final_loop [lemma, in OAut.Buechi]
seq_in_empty_aut_contradicts [lemma, in OAut.Buechi]
seq_eq_index [instance, in OAut.Seqs]
seq_map_proper [instance, in OAut.Seqs]
seq_zip_proper [instance, in OAut.Seqs]
seq_zip [definition, in OAut.Seqs]
seq_map [definition, in OAut.Seqs]
seq_equal_Equivalence [instance, in OAut.Seqs]
seq_equal [definition, in OAut.Seqs]
seq_dec_exists_bounded [instance, in OAut.ASStructures]
setEquiv [definition, in OAut.AbstractMSO]
setless [definition, in OAut.AbstractMSO]
Sets [section, in OAut.AbstractMSO]
setToSeq [definition, in OAut.MSO]
setToSeqCorrect [lemma, in OAut.MSO]
setToSeqExtensional [lemma, in OAut.MSO]
setToSeqExtensional2 [lemma, in OAut.MSO]
setToSeqParitionCorrect [lemma, in OAut.MSO]
setToSeqParitionCorrectInv [lemma, in OAut.MSO]
set_equiv_Equivalence [instance, in OAut.AbstractMSO]
set_equivalent_iff_seq_extensional [lemma, in OAut.MSO]
SEx [constructor, in OAut.AbstractMSO]
sfinal [definition, in OAut.RegularLanguages]
sgBoolAnd [definition, in OAut.Ramsey]
sigT_enum_ok [lemma, in FinTypes.FinTypes]
sigT_proj2_fun [lemma, in FinTypes.BasicDefinitions]
sigT_proj1_fun [lemma, in FinTypes.BasicDefinitions]
Sig_dec [instance, in FinTypes.Automata]
Sig_reach [lemma, in FinTypes.Automata]
singletonSet [projection, in OAut.AbstractMSO]
singletonSetCorrect1 [projection, in OAut.AbstractMSO]
singletonSetCorrect2 [projection, in OAut.AbstractMSO]
singleton_interpretation [lemma, in OAut.AbstractMSO]
singleton_correct2 [lemma, in OAut.AbstractMSO]
singleton_correct [lemma, in OAut.AbstractMSO]
sing_equiv [lemma, in OAut.AbstractMSO]
sinitial [definition, in OAut.RegularLanguages]
SInter [definition, in OAut.AbstractMSO]
SInterExtensional [definition, in OAut.AbstractMSO]
sintersect [definition, in OAut.RegularLanguages]
sintersect_correct [lemma, in OAut.RegularLanguages]
SInter_ext_equiv [instance, in OAut.AbstractMSO]
size_induction [lemma, in FinTypes.External]
slanguage [definition, in OAut.RegularLanguages]
slanguage_extensional [lemma, in OAut.RegularLanguages]
slot_in_smonotone [lemma, in OAut.Ramsey]
SomeElement [lemma, in FinTypes.FinTypes]
some_a [abbreviation, in OAut.NecessityAR]
some_a [abbreviation, in OAut.NecessityAR]
SpecialSeqOperations [section, in OAut.MSO]
special_states [definition, in OAut.RegularLanguages]
split_path [lemma, in OAut.NFAs]
split_final_transforms [lemma, in OAut.Complement]
split_transforms [lemma, in OAut.Complement]
split_position_lang_prepend [lemma, in OAut.Seqs]
split_pos [abbreviation, in OAut.Seqs]
split_string_eq [lemma, in OAut.Seqs]
split_second [definition, in OAut.Seqs]
split_first [definition, in OAut.Seqs]
split_critical_index_begin [lemma, in OAut.ASStructures]
state [abbreviation, in OAut.NecessityAR]
state [abbreviation, in OAut.NecessityAR]
state [projection, in OAut.NFAs]
states_do_not_mix [lemma, in OAut.Buechi]
step [constructor, in FinTypes.Automata]
step_consistent_least_fp [lemma, in FinTypes.FinTypes]
step_trans_fp_incl [lemma, in FinTypes.FinTypes]
step_iter_consistent [lemma, in FinTypes.FinTypes]
step_consistent [definition, in FinTypes.FinTypes]
step_reach_consistent [lemma, in FinTypes.Automata]
step_reach [definition, in FinTypes.Automata]
str [abbreviation, in OAut.NFAs]
Streicher_K [lemma, in FinTypes.BasicDefinitions]
StrictlyMonotoneSeqs [section, in OAut.Seqs]
strict_bounded_exist [instance, in OAut.FinType]
String [record, in OAut.Seqs]
StringLang [abbreviation, in OAut.Seqs]
StringLang_Extensional [definition, in OAut.Seqs]
StringOperationLemmas [section, in OAut.Seqs]
StringOperations [section, in OAut.Seqs]
StringsEq [section, in OAut.Seqs]
StringsOfConstantLength [section, in OAut.Seqs]
StringsOfConstantLength.m [variable, in OAut.Seqs]
strings_equal_Equivalence [instance, in OAut.Seqs]
strings_equal_transitive [lemma, in OAut.Seqs]
strings_equal_symmetric [lemma, in OAut.Seqs]
strings_equal_reflexive [lemma, in OAut.Seqs]
strings_equal [definition, in OAut.Seqs]
stringToList [definition, in OAut.RegularLanguages]
string_final_R' [lemma, in OAut.Complement]
string_omega_omega_iteration [lemma, in OAut.Seqs]
string_zip_snd_up [lemma, in OAut.Seqs]
string_zip_fst_up [lemma, in OAut.Seqs]
string_zip [definition, in OAut.Seqs]
string_map [definition, in OAut.Seqs]
string_lastindex_proper [instance, in OAut.Seqs]
subset [definition, in OAut.AbstractMSO]
subset_proper [instance, in OAut.AbstractMSO]
subtype [definition, in FinTypes.BasicDefinitions]
subType_enum_ok [lemma, in FinTypes.FinTypes]
subType_eq_dec [instance, in FinTypes.BasicDefinitions]
subtype_extensionality [lemma, in FinTypes.BasicDefinitions]
success2 [definition, in FinTypes.FinTypes]
success3 [definition, in FinTypes.FinTypes]
SumCard [lemma, in FinTypes.FinTypes]
sum_enum_ok [lemma, in FinTypes.FinTypes]
sum_eq_dec [instance, in FinTypes.BasicDefinitions]
sum_ramseyan_fac [lemma, in OAut.Ramsey]
sunion [definition, in OAut.RegularLanguages]
sunion_correct [lemma, in OAut.RegularLanguages]
supdate_preserves_singleton [lemma, in OAut.AbstractMSO]
surjective [definition, in FinTypes.BasicDefinitions]
surjectiveApply [lemma, in FinTypes.BasicDefinitions]
surj_sub [lemma, in FinTypes.FinTypes]
svalid [definition, in OAut.RegularLanguages]
SVar [definition, in OAut.AbstractMSO]
swap [definition, in OAut.Seqs]
swap_sum [definition, in OAut.Buechi]
switch_from_V_to_W [lemma, in OAut.Buechi]
s_s'_pair_aut_correct [lemma, in OAut.Complement]
s_s'_pair_aut [definition, in OAut.Complement]
s_monotone_begin_in [lemma, in OAut.Seqs]
s_monotone_drop [lemma, in OAut.Seqs]
s_monotone_ge_zero' [lemma, in OAut.Seqs]
s_monotone_ge_zero [lemma, in OAut.Seqs]
s_monotone_order_preserving_backwards [lemma, in OAut.Seqs]
s_monotone_order_preserving [lemma, in OAut.Seqs]
s_monotone_strict_order_preserving [lemma, in OAut.Seqs]
s_monotone_strict_order_preserving' [lemma, in OAut.Seqs]
s_monotone_ge [lemma, in OAut.Seqs]
s_monotone_unbouded [lemma, in OAut.Seqs]
s_monotone_unbouded_ge [lemma, in OAut.Seqs]
s_monotone_id [lemma, in OAut.Seqs]
s_monotone [definition, in OAut.Seqs]
S_z_minus_1 [lemma, in OAut.BasicDefs]

T

Test [section, in FinTypes.FinTypes]
test [lemma, in OAut.ASStructures]
Test.X [variable, in FinTypes.FinTypes]
Test.Y [variable, in FinTypes.FinTypes]
# _ [notation, in FinTypes.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 [instance, in OAut.Complement]
tff_transition [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]
tilde_w_equiv_mso_correct [lemma, in OAut.NecessityAR]
tilde_w_equiv_mso [definition, in OAut.NecessityAR]
tilde_congruence [lemma, in OAut.Complement]
tilde_w_equiv_cc_nat [lemma, in OAut.Ramsey]
tilde_w_equiv_finite_index [lemma, in OAut.Ramsey]
tilde_w_equivalence [instance, in OAut.Ramsey]
tilde_w_index_transitive [lemma, in OAut.Ramsey]
tilde_w_index_symmetric [lemma, in OAut.Ramsey]
tilde_w_index_reflexive [lemma, in OAut.Ramsey]
tilde_w_extend [lemma, in OAut.Ramsey]
tilde_w_equiv [definition, in OAut.Ramsey]
toBool [definition, in FinTypes.BasicDefinitions]
toDFA [definition, in FinTypes.Automata]
toDFA_correct [lemma, in FinTypes.Automata]
toDFA_delta_star_correct2 [lemma, in FinTypes.Automata]
toDFA_delta_star_correct1 [lemma, in FinTypes.Automata]
toDFA_delta_correct [lemma, in FinTypes.Automata]
toDFA_delta [definition, in FinTypes.Automata]
toDFA_F [definition, in FinTypes.Automata]
toeqType [definition, in FinTypes.BasicDefinitions]
toeqTypeCorrect [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_sub [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_sigT [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_list [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_true [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_false [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_empty [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_prod [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_option [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_nat [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_bool [lemma, in FinTypes.BasicDefinitions]
toeqTypeCorrect_unit [lemma, in FinTypes.BasicDefinitions]
toeqType_idempotent [lemma, in FinTypes.BasicDefinitions]
toeqType_sum [lemma, in FinTypes.BasicDefinitions]
tofinType [definition, in FinTypes.FinTypes]
toFinTypeFromList [definition, in OAut.FinType]
toFinTypeFromListEq [lemma, in OAut.FinType]
tofinType_sub_correct [lemma, in FinTypes.FinTypes]
tofinType_sigT_correct [lemma, in FinTypes.FinTypes]
tofinType_vector_correct [lemma, in FinTypes.FinTypes]
tofinType_idempotent [lemma, in FinTypes.FinTypes]
tofinType_works [lemma, in FinTypes.FinTypes]
toL_A [definition, in OAut.ASStructures]
toMinMSO [definition, in OAut.AbstractMSO]
toNFA [definition, in FinTypes.Automata]
toNFA_correct [lemma, in FinTypes.Automata]
toNFA_delta_star_correct [lemma, in FinTypes.Automata]
toOptionList [definition, in FinTypes.BasicDefinitions]
top [definition, in OAut.AbstractMSO]
toProp [definition, in FinTypes.Automata]
toProp_dec [instance, in FinTypes.Automata]
top_correct [lemma, in OAut.AbstractMSO]
toSigTList [definition, in FinTypes.FinTypes]
toSigTList_count [lemma, in FinTypes.FinTypes]
toSubList [definition, in FinTypes.FinTypes]
toSubList_count [lemma, in FinTypes.FinTypes]
toSumList1 [definition, in FinTypes.BasicDefinitions]
toSumList1_missing [lemma, in FinTypes.BasicDefinitions]
toSumList1_count [lemma, in FinTypes.BasicDefinitions]
toSumList2 [definition, in FinTypes.BasicDefinitions]
toSumList2_missing [lemma, in FinTypes.BasicDefinitions]
toSumList2_count [lemma, in FinTypes.BasicDefinitions]
totality [projection, in OAut.ASStructures]
toV1 [definition, in OAut.AbstractMSO]
toV1Different [lemma, in OAut.AbstractMSO]
toV1Double [lemma, in OAut.AbstractMSO]
toV1Injective [lemma, in OAut.AbstractMSO]
toV1_even [lemma, in OAut.AbstractMSO]
toV2 [definition, in OAut.AbstractMSO]
toV2Different [lemma, in OAut.AbstractMSO]
toV2Double [lemma, in OAut.AbstractMSO]
toV2Injective [lemma, in OAut.AbstractMSO]
toV2_not_even [lemma, in OAut.AbstractMSO]
to_ind_nfa_correct [lemma, in OAut.RegularLanguages]
to_ind_nfa [definition, in OAut.RegularLanguages]
to_min_mso_complete [lemma, in OAut.AbstractMSO]
to_min_mso_sings [lemma, in OAut.AbstractMSO]
to_min_mso_correct [lemma, in OAut.AbstractMSO]
to_seq_unchanged' [lemma, in OAut.Seqs]
to_seq_unchanged [lemma, in OAut.Seqs]
to_bounded_unchanged [lemma, in OAut.Seqs]
to_bounded [definition, in OAut.Seqs]
to_seq [definition, in OAut.Seqs]
transforms [definition, in OAut.Complement]
transformsBehavior [abbreviation, in OAut.Complement]
transforms_final_extensional [instance, in OAut.Complement]
transforms_extensional [instance, in OAut.Complement]
transforms_final [definition, in OAut.Complement]
transition [projection, in OAut.NFAs]
TransitionGraph [section, in OAut.NFAs]
TransitionGraph.InfConcat [section, in OAut.NFAs]
TransitionGraph.InfConcat.runs [variable, in OAut.NFAs]
TransitionGraph.InfConcat.strings [variable, in OAut.NFAs]
transition_all [definition, in OAut.NecessityAR]
transition_at_least_one [definition, in OAut.NecessityAR]
transition_dec_public [instance, in OAut.NFAs]
transition_dec [projection, in OAut.NFAs]
True_dec [instance, in FinTypes.External]
True_enum_ok [lemma, in FinTypes.FinTypes]
True_eq_dec [instance, in FinTypes.BasicDefinitions]
type [projection, in FinTypes.FinTypes]

U

U [definition, in FinTypes.Automata]
UltimatelyPeriodicSequences [section, in OAut.Seqs]
UltimatelyPeriodicSequences.Basic [section, in OAut.Seqs]
UltimatelyPeriodicSequences.StringZip [section, in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip [section, in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip'' [section, in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip''.a [variable, in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip''.b [variable, in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip.a [variable, in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip.b [variable, in OAut.Seqs]
_ ==== _ [notation, in OAut.Seqs]
undup [definition, in FinTypes.External]
Undup [section, in FinTypes.External]
undup_idempotent [lemma, in FinTypes.External]
undup_id [lemma, in FinTypes.External]
undup_equi [lemma, in FinTypes.External]
undup_incl [lemma, in FinTypes.External]
undup_id_equi [lemma, in FinTypes.External]
Undup.X [variable, in FinTypes.External]
unfold [definition, in OAut.Seqs]
unfold_proper [instance, in OAut.Seqs]
union [definition, in OAut.Buechi]
UnionClosure [section, in OAut.Buechi]
UnionClosure.Def [section, in OAut.Buechi]
UnionClosure.Def.aut_2 [variable, in OAut.Buechi]
UnionClosure.Def.aut_1 [variable, in OAut.Buechi]
union_correct [lemma, in OAut.Buechi]
union_symmetric [lemma, in OAut.Buechi]
union_symmetric_acc [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]
union_acorrect [lemma, in OAut.ASStructures]
Unique [definition, in OAut.MSO]
unique_correct [lemma, in OAut.MSO]
unit_enum_ok [lemma, in FinTypes.FinTypes]
unit_eq_dec [instance, in FinTypes.BasicDefinitions]
UniversalBuechiAutomaton [section, in OAut.Buechi]
universal_language [definition, in OAut.BasicDefs]
univ_aut_scorrect [lemma, in OAut.RegularLanguages]
univ_aut [definition, in OAut.NFAs]
univ_aut_correct [lemma, in OAut.Buechi]
UPAdmissible [section, in OAut.ASStructures]
UPAdmissible.PeriodicRun [section, in OAut.ASStructures]
UPAdmissible.PeriodicRun.aut [variable, in OAut.ASStructures]
UPAdmissible.PeriodicRun.vw [variable, in OAut.ASStructures]
update [abbreviation, in OAut.NecessityAR]
update_proper [instance, in OAut.AbstractMSO]
UPDet [definition, in OAut.NecessityAR]
upgrade_bound [definition, in OAut.FinType]
UPSeq [record, in OAut.Seqs]
UPSequenceStructure [definition, in OAut.ASStructures]
UPStructure [definition, in OAut.ASStructures]
up_eq_compl [lemma, in OAut.NecessityAR]
up_equiv_iff_omega_equiv [lemma, in OAut.MSO]
up_sat_iff_omega_sat [lemma, in OAut.MSO]
up_buechi_nonempty_iff_buechi_nonempty [lemma, in OAut.MSO]
up_classic [instance, in OAut.MSO]
up_sat [abbreviation, in OAut.MSO]
up_zip_proper [instance, in OAut.Seqs]
up_zip_correct [lemma, in OAut.Seqs]
up_zip_proj2 [lemma, in OAut.Seqs]
up_zip_proj1 [lemma, in OAut.Seqs]
up_zip [definition, in OAut.Seqs]
up_zip''_proj2 [lemma, in OAut.Seqs]
up_zip''_proj1 [lemma, in OAut.Seqs]
up_zip'' [definition, in OAut.Seqs]
up_zip'_prefix_length [lemma, in OAut.Seqs]
up_zip'_equiv [lemma, in OAut.Seqs]
up_zip' [definition, in OAut.Seqs]
up_map_proper [instance, in OAut.Seqs]
up_loop [lemma, in OAut.Seqs]
up_prefix [lemma, in OAut.Seqs]
up_map_correct [lemma, in OAut.Seqs]
up_map [definition, in OAut.Seqs]
up_equal_Equivalence [instance, in OAut.Seqs]
up_equal [definition, in OAut.Seqs]
up_admits_ramseyan_fac [lemma, in OAut.Ramsey]
U_correct [lemma, in FinTypes.Automata]

V

valid_triple [abbreviation, in OAut.NFAs]
valid_path_reachable [lemma, in OAut.NFAs]
valid_run_reachable [lemma, in OAut.NFAs]
valid_path_cut [lemma, in OAut.NFAs]
valid_prepend_path [lemma, in OAut.NFAs]
valid_prepend_path' [lemma, in OAut.NFAs]
valid_concat_paths [lemma, in OAut.NFAs]
valid_path_is_path_everywhere [lemma, in OAut.NFAs]
valid_run_is_path_everywhere [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_path_decrease' [lemma, in OAut.NFAs]
valid_run_is_path_from_begin [lemma, in OAut.NFAs]
valid_path_proper [instance, in OAut.NFAs]
valid_run_proper [instance, in OAut.NFAs]
valid_path_extensional [lemma, in OAut.NFAs]
valid_run_extensional [lemma, in OAut.NFAs]
valid_path [definition, in OAut.NFAs]
valid_run [definition, in OAut.NFAs]
valid_r' [lemma, in OAut.Complement]
valid_periodic_run [lemma, in OAut.ASStructures]
valid_path_prepended_string [lemma, in OAut.ASStructures]
vars_for_elems_bound [lemma, in OAut.NecessityAR]
vars_for_elems_injective [lemma, in OAut.NecessityAR]
vars_for_list_injective [lemma, in OAut.NecessityAR]
vars_for_list_bound [lemma, in OAut.NecessityAR]
vars_for_list_ge [lemma, in OAut.NecessityAR]
vars_for_elems [definition, in OAut.NecessityAR]
vars_for_list [definition, in OAut.NecessityAR]
vector [definition, in FinTypes.FinTypes]
vectorise [definition, in FinTypes.FinTypes]
vectorise_apply_inverse [lemma, in FinTypes.FinTypes]
vectorise_apply_inverse' [lemma, in FinTypes.FinTypes]
Vectors [section, in OAut.FinType]
Vectors.ConvertRemNotIn [section, in OAut.FinType]
Vectors.ConvertRemNotIn.M [variable, in OAut.FinType]
Vectors.Narrowing [section, in OAut.FinType]
Vectors.Narrowing.P [variable, in OAut.FinType]
Vector_Card [lemma, in FinTypes.FinTypes]
vector_extensionality [lemma, in FinTypes.FinTypes]
vector_enum_ok [lemma, in FinTypes.FinTypes]
vector_eq_dec [instance, in FinTypes.FinTypes]
vector_eq [lemma, in OAut.FinType]
visits_final [definition, in OAut.Complement]
vP [abbreviation, in OAut.NecessityAR]
vv_omega_unfold [lemma, in OAut.Seqs]
VW_part_of_complement [definition, in OAut.Complement]
VW_aut_correct [lemma, in OAut.Complement]
VW_aut [definition, in OAut.Complement]
vX [abbreviation, in OAut.NecessityAR]
vX_vP_disjoint [lemma, in OAut.NecessityAR]
v_transforms [lemma, in OAut.Complement]
v'_transforms [lemma, in OAut.Complement]

W

word [definition, in FinTypes.Automata]
wrap_string [lemma, in OAut.Seqs]
W_transforms [lemma, in OAut.Complement]
W_final_iff [lemma, in OAut.Complement]
W_final [definition, in OAut.Complement]
W'_transforms [lemma, in OAut.Complement]

X

XinA [lemma, in OAut.MSO]
XMWordProblemImpliesInfinitePigeonholePrinciple [section, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.A [variable, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AllNotNFA [section, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AllNotNFA.a [variable, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AllNotNFA.A [variable, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AtLeastOneNFA [section, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AtLeastOneNFA.a [variable, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AtLeastOneNFA.A [variable, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.FiniteAut [section, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.FiniteAut.a [variable, in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.xm_word_problem [variable, in OAut.NecessityAR]
XM_WordProblem [definition, in OAut.NecessityAR]
xm_word_problem [lemma, in OAut.ASStructures]
XM_implies_RamseyFac [lemma, in OAut.Ramsey]

Y

YinA [lemma, in OAut.MSO]

Z

ZeroEl [definition, in OAut.AbstractMSO]
zeroElCorrect [lemma, in OAut.AbstractMSO]
zipFinTypes [definition, in OAut.ASStructures]
zip_existential [lemma, in OAut.MSO]

other

_ ** _ (EqTypeScope) [notation, in FinTypes.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 FinTypes.External]
_ === _ [notation, in FinTypes.External]
_ <<= _ [notation, in FinTypes.External]
_ el _ [notation, in FinTypes.External]
_ ^ _ [notation, in FinTypes.FinTypes]
_ --> _ [notation, in FinTypes.FinTypes]
_ (+) _ [notation, in FinTypes.FinTypes]
_ (x) _ [notation, in FinTypes.FinTypes]
_ ==>2 _ [notation, in OAut.AbstractMSO]
_ \/2 _ [notation, in OAut.AbstractMSO]
_ =~~= _ [notation, in OAut.AbstractMSO]
_ <=2 _ [notation, in OAut.AbstractMSO]
_ |= _ [notation, in OAut.AbstractMSO]
_ # _ |== _ [notation, in OAut.AbstractMSO]
_ [ _ := _ ] [notation, in OAut.AbstractMSO]
_ =~= _ [notation, in OAut.AbstractMSO]
_ /\2 _ [notation, in OAut.AbstractMSO]
_ <<=2 _ [notation, in OAut.AbstractMSO]
_ el2 _ [notation, in OAut.AbstractMSO]
_ <2 _ [notation, in OAut.AbstractMSO]
_ /\0 _ [notation, in OAut.AbstractMSO]
_ <<=0 _ [notation, in OAut.AbstractMSO]
_ <0 _ [notation, in OAut.AbstractMSO]
_ [ _ := _ ] [notation, in OAut.AbstractMSO]
_ =~= _ [notation, in OAut.AbstractMSO]
_ elS _ [notation, in OAut.AbstractMSO]
_ ** _ [notation, in FinTypes.BasicDefinitions]
_ o _ [notation, in OAut.Seqs]
_ ^00 [notation, in OAut.Seqs]
_ ^0$0 [notation, in OAut.Seqs]
_ to_omega [notation, in OAut.Seqs]
_ === _ [notation, in OAut.Seqs]
_ ==== _ [notation, in OAut.ASStructures]
_ ^^ _ [notation, in OAut.FinType]
_ ^$~ [notation, in OAut.BasicDefs]
_ /$\ _ [notation, in OAut.BasicDefs]
_ \$/ _ [notation, in OAut.BasicDefs]
_ =$= _ [notation, in OAut.BasicDefs]
_ <$= _ [notation, in OAut.BasicDefs]
all1 _ , _ [notation, in OAut.AbstractMSO]
all2 _ , _ [notation, in OAut.AbstractMSO]
AND { ( _ , _ ) | _ } _ [notation, in OAut.AbstractMSO]
AND { _ | _ } _ [notation, in OAut.AbstractMSO]
eq_dec _ [notation, in FinTypes.External]
ex0 _ , _ [notation, in OAut.AbstractMSO]
ex1 _ , _ [notation, in OAut.AbstractMSO]
ex2 _ , _ [notation, in OAut.AbstractMSO]
L_S [notation, in OAut.RegularLanguages]
L_B [notation, in OAut.Buechi]
OR { ( _ , _ , _ ) | _ } _ [notation, in OAut.AbstractMSO]
OR { _ | _ } _ [notation, in OAut.AbstractMSO]
# _ [notation, in FinTypes.FinTypes]
? _ [notation, in FinTypes.FinTypes]
?? _ [notation, in FinTypes.BasicDefinitions]
{[ _ ]} [notation, in OAut.ASStructures]
{} [notation, in OAut.BasicDefs]
| _ | [notation, in FinTypes.External]
~0 _ [notation, in OAut.AbstractMSO]
~2 _ [notation, in OAut.AbstractMSO]

Notation Index

B

_ ==== _ [in OAut.ASStructures]
_ ~~ _ [in OAut.Complement]
_ =!=> _ on _ [in OAut.Complement]
_ ===> _ on _ [in OAut.Complement]
{[ _ ]} [in OAut.Complement]

D

_ ~~# _ [in OAut.Ramsey]
_ ~~@ _ at _ [in OAut.Ramsey]

M

_ ~~# _ [in OAut.NecessityAR]
_ ~~@ _ at _ [in OAut.NecessityAR]
InclS [in OAut.MSO]
NotInclS [in OAut.MSO]
Less [in OAut.MSO]
SearchX [in OAut.MSO]
SearchY [in OAut.MSO]
A [in OAut.MSO]
L_M [in OAut.MSO]
<< _ , _ >> [in OAut.AbstractMSO]
<\ _ |> [in OAut.AbstractMSO]
<| _ /> [in OAut.AbstractMSO]
[ _ ] [in OAut.AbstractMSO]
_ =~~= _ [in OAut.AbstractMSO]
_ # _ |== _ [in OAut.AbstractMSO]
_ |= _ [in OAut.AbstractMSO]

N

Final [in OAut.RegularLanguages]
Initial [in OAut.RegularLanguages]

T

# _ [in FinTypes.FinTypes]

U

_ ==== _ [in OAut.Seqs]

other

_ ** _ (EqTypeScope) [in FinTypes.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 FinTypes.External]
_ === _ [in FinTypes.External]
_ <<= _ [in FinTypes.External]
_ el _ [in FinTypes.External]
_ ^ _ [in FinTypes.FinTypes]
_ --> _ [in FinTypes.FinTypes]
_ (+) _ [in FinTypes.FinTypes]
_ (x) _ [in FinTypes.FinTypes]
_ ==>2 _ [in OAut.AbstractMSO]
_ \/2 _ [in OAut.AbstractMSO]
_ =~~= _ [in OAut.AbstractMSO]
_ <=2 _ [in OAut.AbstractMSO]
_ |= _ [in OAut.AbstractMSO]
_ # _ |== _ [in OAut.AbstractMSO]
_ [ _ := _ ] [in OAut.AbstractMSO]
_ =~= _ [in OAut.AbstractMSO]
_ /\2 _ [in OAut.AbstractMSO]
_ <<=2 _ [in OAut.AbstractMSO]
_ el2 _ [in OAut.AbstractMSO]
_ <2 _ [in OAut.AbstractMSO]
_ /\0 _ [in OAut.AbstractMSO]
_ <<=0 _ [in OAut.AbstractMSO]
_ <0 _ [in OAut.AbstractMSO]
_ [ _ := _ ] [in OAut.AbstractMSO]
_ =~= _ [in OAut.AbstractMSO]
_ elS _ [in OAut.AbstractMSO]
_ ** _ [in FinTypes.BasicDefinitions]
_ o _ [in OAut.Seqs]
_ ^00 [in OAut.Seqs]
_ ^0$0 [in OAut.Seqs]
_ to_omega [in OAut.Seqs]
_ === _ [in OAut.Seqs]
_ ==== _ [in OAut.ASStructures]
_ ^^ _ [in OAut.FinType]
_ ^$~ [in OAut.BasicDefs]
_ /$\ _ [in OAut.BasicDefs]
_ \$/ _ [in OAut.BasicDefs]
_ =$= _ [in OAut.BasicDefs]
_ <$= _ [in OAut.BasicDefs]
all1 _ , _ [in OAut.AbstractMSO]
all2 _ , _ [in OAut.AbstractMSO]
AND { ( _ , _ ) | _ } _ [in OAut.AbstractMSO]
AND { _ | _ } _ [in OAut.AbstractMSO]
eq_dec _ [in FinTypes.External]
ex0 _ , _ [in OAut.AbstractMSO]
ex1 _ , _ [in OAut.AbstractMSO]
ex2 _ , _ [in OAut.AbstractMSO]
L_S [in OAut.RegularLanguages]
L_B [in OAut.Buechi]
OR { ( _ , _ , _ ) | _ } _ [in OAut.AbstractMSO]
OR { _ | _ } _ [in OAut.AbstractMSO]
# _ [in FinTypes.FinTypes]
? _ [in FinTypes.FinTypes]
?? _ [in FinTypes.BasicDefinitions]
{[ _ ]} [in OAut.ASStructures]
{} [in OAut.BasicDefs]
| _ | [in FinTypes.External]
~0 _ [in OAut.AbstractMSO]
~2 _ [in OAut.AbstractMSO]

Variable Index

B

BuechiAutomaton.aut [in OAut.Buechi]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsFinalRecognizable.endS [in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsFinalRecognizable.startS [in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsRecognizable.endS [in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsRecognizable.startS [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.Acc [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.agree_R [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.agree_r0 [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.eqLengthv [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.inV [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.inV' [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.inW [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.inW' [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.R [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.r0 [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.V [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.v [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.valid_R [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.valid_r0 [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.v' [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.W [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.w [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility.w' [in OAut.Complement]

C

Cardinality.X [in FinTypes.External]
ClosureProperties.AC [in OAut.ASStructures]
ClosureProperties.Complement.aut [in OAut.ASStructures]
ClosureProperties.X [in OAut.ASStructures]
ClosureProperties.Y [in OAut.ASStructures]
ClosureUnderComplementImpliesAdditiveRamsey.complement [in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.RamseyNFA.RamseyNFAIdem.x [in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.xm_word_problem [in OAut.NecessityAR]
Complement.A [in OAut.Complement]
Complement.aut [in OAut.Complement]
ConcatInfPrependNFA.runs [in OAut.Buechi]
ConcatInfPrependNFA.strings [in OAut.Buechi]
ConvertToNFA.aut [in OAut.RegularLanguages]

D

DecBuechiAutomatonEmpty.aut [in OAut.Buechi]
DeriveRamseyFac.f [in OAut.Ramsey]
DeriveRamseyFac.INF_DM [in OAut.Ramsey]
DeriveRamseyFac.IPP_DM [in OAut.Ramsey]
DFA.Operations.A [in FinTypes.Automata]
DFA.Operations.A' [in FinTypes.Automata]
DFA.Operations.Product_automaton.op_dec [in FinTypes.Automata]
DFA.Operations.Product_automaton.op [in FinTypes.Automata]
DFA.Reachability.A [in FinTypes.Automata]
DFA.Sig [in FinTypes.Automata]
DupFreeDis.X [in FinTypes.External]
Dupfree.X [in FinTypes.External]

E

Equi.X [in FinTypes.External]

F

FilterLemmas_pq.q [in FinTypes.External]
FilterLemmas_pq.p [in FinTypes.External]
FilterLemmas_pq.X [in FinTypes.External]
FilterLemmas.p [in FinTypes.External]
FilterLemmas.X [in FinTypes.External]
FindNextPosition.NextPositionExists.L [in OAut.Seqs]
FindNextPosition.NextPosition.F [in OAut.Seqs]
FindNextPosition.NextPosition.L [in OAut.Seqs]
FindNextPosition.P [in OAut.Seqs]
FindNextPosition.w [in OAut.Seqs]
FiniteClosureIteration.step [in FinTypes.FinTypes]
FiniteClosureIteration.step_dec [in FinTypes.FinTypes]
FiniteClosureIteration.X [in FinTypes.FinTypes]
First.p [in OAut.BasicDefs]
First.p_dec [in OAut.BasicDefs]
Fixedpoints.f [in FinTypes.FinTypes]
Fixedpoints.X [in FinTypes.FinTypes]

I

ImageNFA.aut [in OAut.Buechi]
ImageNFA.f [in OAut.Buechi]
Inclusion.X [in FinTypes.External]
InfiniteFilter.infP [in OAut.Seqs]
InfiniteFilter.P [in OAut.Seqs]
InfiniteFilter.w [in OAut.Seqs]
IntersectionClosure.aut_2 [in OAut.Buechi]
IntersectionClosure.aut_1 [in OAut.Buechi]
IntersectionClosure.IRun.F1 [in OAut.Buechi]
IntersectionClosure.IRun.F2 [in OAut.Buechi]
IntersectionClosure.IRun.r_2 [in OAut.Buechi]
IntersectionClosure.IRun.r_1 [in OAut.Buechi]
IntersectionClosure.IRun.w [in OAut.Buechi]

L

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

M

Membership.X [in FinTypes.External]
MSOClassicalImpliesRamseyFac.ADD_Formula.vP [in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.ADD_Formula.vX [in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.f [in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.MSO_XM [in OAut.NecessityAR]
MSOtoBuechi.BaseNFAs.X [in OAut.MSO]
MSOtoBuechi.BaseNFAs.Y [in OAut.MSO]

N

NFAOmegaIteration.OmegaIterNormalized.aut [in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized.finalW [in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized.initialW [in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized.normW [in OAut.Buechi]
NormalizeNFA.aut [in OAut.RegularLanguages]

O

OneStringNFA.v [in OAut.RegularLanguages]

P

PowerRep.X [in FinTypes.External]
PreImageNFA.aut [in OAut.Buechi]
PreImageNFA.f [in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.aut_2 [in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.aut_1 [in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.finalV [in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.initialV [in OAut.Buechi]
PrependNFA.PrependNormalizedNFA.norm [in OAut.Buechi]

Q

Quotients.E [in OAut.FinType]
Quotients.EisEquiv [in OAut.FinType]

R

Removal.X [in FinTypes.External]

S

StringsOfConstantLength.m [in OAut.Seqs]

T

Test.X [in FinTypes.FinTypes]
Test.Y [in FinTypes.FinTypes]
TransitionGraph.InfConcat.runs [in OAut.NFAs]
TransitionGraph.InfConcat.strings [in OAut.NFAs]

U

UltimatelyPeriodicSequences.UPZip''.a [in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip''.b [in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip.a [in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip.b [in OAut.Seqs]
Undup.X [in FinTypes.External]
UnionClosure.Def.aut_2 [in OAut.Buechi]
UnionClosure.Def.aut_1 [in OAut.Buechi]
UPAdmissible.PeriodicRun.aut [in OAut.ASStructures]
UPAdmissible.PeriodicRun.vw [in OAut.ASStructures]

V

Vectors.ConvertRemNotIn.M [in OAut.FinType]
Vectors.Narrowing.P [in OAut.FinType]

X

XMWordProblemImpliesInfinitePigeonholePrinciple.A [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AllNotNFA.a [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AllNotNFA.A [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AtLeastOneNFA.a [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AtLeastOneNFA.A [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.FiniteAut.a [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.xm_word_problem [in OAut.NecessityAR]

Library Index

A

AbstractMSO
ASStructures
Automata

B

BasicDefinitions
BasicDefs
Buechi

C

Complement

E

External

F

FinType
FinTypes

M

MSO

N

NecessityAR
NFAs

R

Ramsey
RegularLanguages

S

Seqs

Lemma Index

A

accepting_all [in OAut.NecessityAR]
accepting_extensional [in OAut.Buechi]
accepting_run_for_W' [in OAut.Complement]
accepting_implies_less [in OAut.MSO]
accepting_run_less [in OAut.MSO]
accepting_run_search_Y [in OAut.MSO]
accepting_applies_incl [in OAut.MSO]
addEqClass_is_associative [in OAut.Complement]
addEqClass_is_additive [in OAut.Complement]
additiveRamsey_implies_mso_classical [in OAut.NecessityAR]
additiveRamsey_implies_compl [in OAut.NecessityAR]
additive_ramsey_iff_ramsey_fac [in OAut.NecessityAR]
ADD_formula_correct [in OAut.NecessityAR]
ADD_formula'_correct [in OAut.NecessityAR]
ADD_extract_last [in OAut.Ramsey]
ADD_single_extract [in OAut.Ramsey]
ADD_iter [in OAut.Ramsey]
ADD_split [in OAut.Ramsey]
ADD'_last [in OAut.Ramsey]
ADD'_extensional [in OAut.Ramsey]
admits_ramseyan_fac_iff_idem_ramseyan_fac [in OAut.Ramsey]
allSub [in FinTypes.FinTypes]
all_finite_impossible [in OAut.NecessityAR]
all_fin_nfa_correct [in OAut.NecessityAR]
all_not_nfa_correct [in OAut.NecessityAR]
all1_correct [in OAut.AbstractMSO]
all2_correct [in OAut.AbstractMSO]
and_correct [in OAut.AbstractMSO]
appendNil [in FinTypes.BasicDefinitions]
apply_vectorise_inverse [in FinTypes.FinTypes]
at_least_one_nfa_correct [in OAut.NecessityAR]
at_most_one_eq_class [in OAut.Complement]
autC_disjoint [in OAut.ASStructures]
autU_accepted_by_aut1 [in OAut.Buechi]
aut_accepts_normalize [in OAut.RegularLanguages]
aut_accepts_nfa_omega_iter' [in OAut.Buechi]
aut_accepts_image [in OAut.Buechi]
aut1_incl_autU [in OAut.Buechi]

B

begin_in_equal [in OAut.Seqs]
between_final_state_intersect_is_final_state_aut_1 [in OAut.Buechi]
bigAndCorrect [in OAut.AbstractMSO]
bigEx2_correct [in OAut.AbstractMSO]
bigOrCorrect [in OAut.AbstractMSO]
bigpi_correct [in OAut.ASStructures]
bigUpdate2_update [in OAut.AbstractMSO]
bigUpdate2_unchanged [in OAut.AbstractMSO]
bigzip_correct [in OAut.ASStructures]
bigzip_correct' [in OAut.ASStructures]
big_intersection_scorrect [in OAut.RegularLanguages]
big_intersection_compl_correct [in OAut.NecessityAR]
big_intersection_correct [in OAut.Buechi]
big_union_correct [in OAut.Buechi]
big_union_acorrect [in OAut.ASStructures]
big_and_false [in OAut.Ramsey]
big_and_true [in OAut.Ramsey]
boolOption_enum_ok [in FinTypes.FinTypes]
bool_enum_ok [in FinTypes.FinTypes]
bot_correct [in OAut.AbstractMSO]
bounded_path_iff_path [in OAut.NFAs]
bounded_run_is_valid_path [in OAut.NFAs]
bounded_unchanged_string [in OAut.Seqs]
bounded_unchanged [in OAut.Seqs]
buechi_equiv_class_NFA_recognizable [in OAut.Complement]
buechi_equiv_class_NFA_recognizable_MyhillNerode [in OAut.Complement]
buechi_eq_class_correct [in OAut.Complement]

C

can_find_duplicate' [in OAut.Seqs]
can_find_duplicate [in OAut.Seqs]
can_find_next_position [in OAut.Seqs]
CardIn [in FinTypes.FinTypes]
Cardinality_card_eq [in FinTypes.FinTypes]
card_or [in FinTypes.External]
card_lt [in FinTypes.External]
card_equi [in FinTypes.External]
card_ex [in FinTypes.External]
card_0 [in FinTypes.External]
card_cons_rem [in FinTypes.External]
card_eq [in FinTypes.External]
card_le [in FinTypes.External]
card_not_in_rem [in FinTypes.External]
card_in_rem [in FinTypes.External]
card_upper_bound [in FinTypes.FinTypes]
Card_positiv [in FinTypes.FinTypes]
card_length_leq [in FinTypes.BasicDefinitions]
card_finType_Le_K [in OAut.FinType]
card_finTypeC_Le_K [in OAut.FinType]
cc_nat [in OAut.BasicDefs]
cc_nat_first [in OAut.BasicDefs]
Closure [in FinTypes.FinTypes]
closure_complement_implies_finite_type_seq [in OAut.NecessityAR]
Closure_FCIter [in FinTypes.FinTypes]
coincidence [in OAut.AbstractMSO]
combine_final_transforms_right [in OAut.Complement]
combine_final_transforms_left [in OAut.Complement]
combine_transforms [in OAut.Complement]
compact_f [in OAut.Ramsey]
compatibility [in OAut.Complement]
compatibilityComplement [in OAut.Complement]
compatibility2 [in OAut.Complement]
complement_correct [in FinTypes.Automata]
complement_correct2 [in OAut.ASStructures]
complement_correct [in OAut.ASStructures]
complement_complete [in OAut.ASStructures]
complete_induction [in OAut.BasicDefs]
compl_closed_xm_word_problem_implies_ramsey_fac [in OAut.NecessityAR]
compose_s_monotone [in OAut.Seqs]
compute_run_final_transforms [in OAut.Complement]
compute_run_transforms [in OAut.Complement]
concat_paths [in OAut.NFAs]
concat_inf_is_valid' [in OAut.NFAs]
concat_inf_is_valid [in OAut.NFAs]
concat_inf_is_valid'' [in OAut.NFAs]
concat_map_length [in FinTypes.FinTypes]
concat_correct [in FinTypes.Automata]
concat_delta_Q_star_correct4 [in FinTypes.Automata]
concat_delta_Q_star_correct3 [in FinTypes.Automata]
concat_delta_Q_star_correct2 [in FinTypes.Automata]
concat_delta_Q_star_correct1 [in FinTypes.Automata]
concat_inf_infiniteP_inverse [in OAut.Seqs]
concat_inf_infiniteP [in OAut.Seqs]
concat_strings_omega_unfold [in OAut.Seqs]
concat_inf_indices_constant_step' [in OAut.Seqs]
concat_inf_indices_constant_step [in OAut.Seqs]
concat_inf_indices_constant_first [in OAut.Seqs]
concat_inf_indices_step [in OAut.Seqs]
concat_inf_extensional [in OAut.Seqs]
concat_inf_index_equal [in OAut.Seqs]
concat_inf_correct [in OAut.Seqs]
concat_inf_index_to_begin [in OAut.Seqs]
concat_inf_index_injective [in OAut.Seqs]
concat_if_indices_lower_bound [in OAut.Seqs]
concat_inf_index_le [in OAut.Seqs]
concat_inf_index_step_correct [in OAut.Seqs]
concat_inf_index_in_bounds [in OAut.Seqs]
concat_inf_index_correct [in OAut.Seqs]
concat_inf_index_begin [in OAut.Seqs]
concat_inf_index_in_string [in OAut.Seqs]
concat_extract [in OAut.Seqs]
concat_strings_associative [in OAut.Seqs]
concat_prepend_string_associative [in OAut.Seqs]
concat_strings_length [in OAut.Seqs]
concat_strings_step [in OAut.Seqs]
concat_string_rest [in OAut.Seqs]
concat_string_begin [in OAut.Seqs]
consAppend [in FinTypes.BasicDefinitions]
const_correct [in OAut.ASStructures]
cons_correct [in FinTypes.Automata]
cons_incll [in FinTypes.BasicDefinitions]
convRemInv_seqToInter [in OAut.MSO]
convRemInv_correct' [in OAut.FinType]
convRemInv_correct [in OAut.FinType]
countApp [in FinTypes.BasicDefinitions]
countIn [in FinTypes.BasicDefinitions]
countMap [in FinTypes.BasicDefinitions]
countMapExistT [in FinTypes.FinTypes]
countMapExistT_Zero [in FinTypes.FinTypes]
countMapZero [in FinTypes.BasicDefinitions]
countNumberApp [in FinTypes.FinTypes]
countSplit [in FinTypes.BasicDefinitions]
counttFL [in FinTypes.FinTypes]
countZero [in FinTypes.BasicDefinitions]
count_in_equiv [in FinTypes.BasicDefinitions]
cover_correct [in OAut.MSO]
critical_index_unfold_distance' [in OAut.ASStructures]
critical_index_unfold_distance [in OAut.ASStructures]
critical_index_unfold_pred_index [in OAut.ASStructures]
critical_index_unfold_ge_zero [in OAut.ASStructures]
critical_index_unfold_monotone [in OAut.ASStructures]
critical_index_unfold_bound [in OAut.ASStructures]
cut_loop_preserves_last_state [in OAut.NFAs]
cut_loop_preserves_first_state [in OAut.NFAs]
cut_loop_decrease [in OAut.NFAs]
cut_loop_valid [in OAut.NFAs]
cut_rest [in OAut.Seqs]
cut_front [in OAut.Seqs]
cut_string_cut [in OAut.Seqs]
cycle_omega_is_valid_run [in OAut.NFAs]

D

decision_false [in OAut.BasicDefs]
decision_true [in OAut.BasicDefs]
DecRef [in FinTypes.BasicDefinitions]
dec_prop_iff [in FinTypes.External]
dec_DM_all [in FinTypes.External]
dec_DM_impl [in FinTypes.External]
dec_DM_and' [in FinTypes.External]
dec_DM_and [in FinTypes.External]
dec_DN [in FinTypes.External]
dec_trans [in FinTypes.External]
dec_singleton_sets [in OAut.AbstractMSO]
dec_up_in_lang [in OAut.Buechi]
dec_language_empty [in OAut.Buechi]
dec_language_empty_informative [in OAut.Buechi]
dec_language_empty_informative_periodic [in OAut.Buechi]
dec_satisfaction_up [in OAut.MSO]
dec_up_in_lang' [in OAut.MSO]
dec_general_sat [in OAut.MSO]
dec_up_sat [in OAut.MSO]
dec_sat [in OAut.MSO]
dec_language_eq [in OAut.ASStructures]
dec_language_inclusion [in OAut.ASStructures]
dec_language_universal [in OAut.ASStructures]
dec_alanguage_empty [in OAut.ASStructures]
delta_Q_star_trans [in FinTypes.Automata]
delta_star_reach [in FinTypes.Automata]
detlaQstar_convert_inverse [in OAut.RegularLanguages]
detlaQstar_convert [in OAut.RegularLanguages]
detlaQstar_decrease_step [in OAut.RegularLanguages]
diff_correct [in FinTypes.Automata]
disjoint_app [in FinTypes.External]
disjoint_cons [in FinTypes.External]
disjoint_nil' [in FinTypes.External]
disjoint_nil [in FinTypes.External]
disjoint_incl [in FinTypes.External]
disjoint_symm [in FinTypes.External]
disjoint_forall [in FinTypes.External]
disjoint_in_map_map_cons [in FinTypes.FinTypes]
disjoint_in [in FinTypes.FinTypes]
disjoint_map_cons [in FinTypes.FinTypes]
disjoint_concat [in FinTypes.FinTypes]
divToV1 [in OAut.AbstractMSO]
divToV2 [in OAut.AbstractMSO]
DM_not_exists [in FinTypes.External]
DM_or [in FinTypes.External]
DM_exists [in FinTypes.FinTypes]
DM_notAll [in FinTypes.FinTypes]
drop_preserves_infinite [in OAut.Seqs]
drop_preserves_infiniteP [in OAut.Seqs]
drop_extract [in OAut.Seqs]
drop_correct'' [in OAut.Seqs]
drop_correct' [in OAut.Seqs]
drop_correct [in OAut.Seqs]
dummy [in OAut.Seqs]
dupfreeCount [in FinTypes.BasicDefinitions]
dupfree_in_power [in FinTypes.External]
dupfree_power [in FinTypes.External]
dupfree_undup [in FinTypes.External]
dupfree_card [in FinTypes.External]
dupfree_dec [in FinTypes.External]
dupfree_filter [in FinTypes.External]
dupfree_map [in FinTypes.External]
dupfree_app [in FinTypes.External]
dupfree_cons [in FinTypes.External]
dupfree_FCIter [in FinTypes.FinTypes]
dupfree_iterstep [in FinTypes.FinTypes]
dupfree_FCStep [in FinTypes.FinTypes]
dupfree_concat_map_cons [in FinTypes.FinTypes]
dupfree_concat [in FinTypes.FinTypes]
dupfree_length [in FinTypes.FinTypes]
dupfree_elements [in FinTypes.FinTypes]
dupfree_countOne [in FinTypes.FinTypes]
dupfree_injective_map [in OAut.FinType]

E

elementIn [in FinTypes.FinTypes]
el_correct [in OAut.AbstractMSO]
Empty_set_enum_ok [in FinTypes.FinTypes]
empty_reach [in FinTypes.Automata]
empty_aut_correct [in OAut.Buechi]
empty_aut_acorrect [in OAut.ASStructures]
enum_ok_fromList [in FinTypes.FinTypes]
Epsilon_autom_correct [in FinTypes.Automata]
equalSELangImpliesEqualSLang [in OAut.Complement]
Equivalence_property_exists' [in FinTypes.FinTypes]
Equivalence_property_exists [in FinTypes.FinTypes]
Equivalence_property_all [in FinTypes.FinTypes]
equivalent_in_equivalence_class [in OAut.Complement]
equivalent_in_equivalence_class' [in OAut.Complement]
equiv_unsat [in OAut.AbstractMSO]
equiv_merge_subseq_merge_at_next [in OAut.Ramsey]
equiv_merge_subseq_s_monotone [in OAut.Ramsey]
equi_rotate [in FinTypes.External]
equi_shift [in FinTypes.External]
equi_swap [in FinTypes.External]
equi_dup [in FinTypes.External]
equi_push [in FinTypes.External]
eq_iff [in FinTypes.FinTypes]
eq_funTrans [in FinTypes.BasicDefinitions]
eq_classes_extensional [in OAut.Complement]
eq_string_access' [in OAut.Seqs]
eq_string_access [in OAut.Seqs]
exactW_correct [in FinTypes.Automata]
exact_up_nfa_correct [in OAut.Buechi]
extPow_length [in FinTypes.FinTypes]
extract_omega_iter [in OAut.Seqs]
extract_concat_inf [in OAut.Seqs]
extract_prepend [in OAut.Seqs]
extract_from_drop' [in OAut.Seqs]
extract_from_drop [in OAut.Seqs]
extract_correct [in OAut.Seqs]

F

False_enum_ok [in FinTypes.FinTypes]
FCIter_ind [in FinTypes.FinTypes]
FCIter_fp [in FinTypes.FinTypes]
FCStep_admissible [in FinTypes.FinTypes]
filter_comm [in FinTypes.External]
filter_and [in FinTypes.External]
filter_pq_eq [in FinTypes.External]
filter_pq_mono [in FinTypes.External]
filter_fst' [in FinTypes.External]
filter_fst [in FinTypes.External]
filter_app [in FinTypes.External]
filter_id [in FinTypes.External]
filter_mono [in FinTypes.External]
filter_incl [in FinTypes.External]
final_loop_implies_up_seq [in OAut.Buechi]
final_iff_step [in OAut.Buechi]
final_prepend [in OAut.Buechi]
final_drop [in OAut.Buechi]
final_r' [in OAut.Complement]
final_transform_implies_transform [in OAut.Complement]
final_to_critical [in OAut.ASStructures]
final_state_eq [in OAut.ASStructures]
finBigAndCorrect [in OAut.AbstractMSO]
finBigEx2_correct [in OAut.AbstractMSO]
finBigOrCorrect [in OAut.AbstractMSO]
finBigUpdate2_changed [in OAut.AbstractMSO]
finBigUpdate2_unchanged [in OAut.AbstractMSO]
fInduction [in FinTypes.FinTypes]
find_multiplicative [in OAut.ASStructures]
find_pos_begin [in OAut.Ramsey]
finite_prefix_preserves_infinite [in OAut.Seqs]
finite_prefix_preserves_infiniteP [in OAut.Seqs]
finTypeOption_enum [in FinTypes.FinTypes]
finTypeOption_correct [in FinTypes.FinTypes]
finTypeProd_enum [in FinTypes.FinTypes]
finTypeSum_enum [in FinTypes.FinTypes]
finTypeSum_correct [in FinTypes.FinTypes]
finType_fromList_correct [in FinTypes.FinTypes]
finType_sub_enum [in FinTypes.FinTypes]
finType_sub_correct [in FinTypes.FinTypes]
finType_sigT_enum [in FinTypes.FinTypes]
finType_sigT_correct [in FinTypes.FinTypes]
finType_vector_enum [in FinTypes.FinTypes]
finType_vector_correct [in FinTypes.FinTypes]
finType_Prod_correct [in FinTypes.FinTypes]
fin_nfa_correct [in OAut.NecessityAR]
fin_iter_last_index [in OAut.Seqs]
fin_iter_index [in OAut.Seqs]
fin_iter_to_omega [in OAut.Seqs]
fin_iter_fin_iter [in OAut.Seqs]
fin_iter_sum [in OAut.Seqs]
fin_iter_length_bound [in OAut.Seqs]
fin_iter_length [in OAut.Seqs]
fin_iter_split [in OAut.Seqs]
fin_iter_base [in OAut.Seqs]
fin_iter_step [in OAut.Seqs]
first_norm_is_initial [in OAut.RegularLanguages]
first_order_var_singleton [in OAut.AbstractMSO]
fix_first_zero_s_monotone [in OAut.Seqs]
formulaNFA_correct [in OAut.MSO]
formula_language_complete [in OAut.MSO]
fp_admissible [in FinTypes.FinTypes]
fp_card_admissible [in FinTypes.FinTypes]
fp_iter_trans [in FinTypes.FinTypes]
fp_trans [in FinTypes.FinTypes]
freeVarInSingleton [in OAut.AbstractMSO]
free_vars_singleton [in OAut.AbstractMSO]
free_sings_correct [in OAut.AbstractMSO]
free_sings'_correct [in OAut.AbstractMSO]
free_vars_and_incl [in OAut.AbstractMSO]
fromMinMSOInter_fvar [in OAut.AbstractMSO]
fromMinMSOInter_svar [in OAut.AbstractMSO]
fromToFVar [in OAut.AbstractMSO]
fromToSVar [in OAut.AbstractMSO]
from_ind_nfa_correct [in OAut.RegularLanguages]
from_to_fin_type_from_list [in OAut.FinType]
fupfate_preserves_singleton [in OAut.AbstractMSO]

G

getAt_correct [in FinTypes.FinTypes]
getImage_correct [in FinTypes.FinTypes]
getImage_length [in FinTypes.FinTypes]
getImage_in [in FinTypes.FinTypes]
get_equiv_class_correct [in OAut.FinType]
get_equiv_class_rep_unique [in OAut.FinType]
get_equiv_class_rep_less [in OAut.FinType]
get_equiv_class_rep_equiv [in OAut.FinType]
ge_to_le [in OAut.Seqs]

H

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

I

idempotent_mul [in OAut.Ramsey]
imagesDupfree [in FinTypes.FinTypes]
imagesInnerLength [in FinTypes.FinTypes]
imagesNonempty [in FinTypes.FinTypes]
images_length [in FinTypes.FinTypes]
image_aut_correct [in OAut.Buechi]
image_accepts_aut [in OAut.Buechi]
impl_correct [in OAut.AbstractMSO]
incl_app_left [in FinTypes.External]
incl_lrcons [in FinTypes.External]
incl_rcons [in FinTypes.External]
incl_sing [in FinTypes.External]
incl_lcons [in FinTypes.External]
incl_shift [in FinTypes.External]
incl_nil_eq [in FinTypes.External]
incl_map [in FinTypes.External]
incl_nil [in FinTypes.External]
incl_nfa_correct [in OAut.MSO]
incl_implies_accepting [in OAut.MSO]
inConcatCons [in FinTypes.FinTypes]
InCount [in FinTypes.BasicDefinitions]
ind_dfa_to_nfa_correct [in OAut.RegularLanguages]
ind_nfa_to_dfa_correct [in OAut.RegularLanguages]
infinite_equiv_indices_dm [in OAut.NecessityAR]
infinite_final_strings_R [in OAut.Complement]
infinite_filter_zero [in OAut.Seqs]
infinite_filter_all [in OAut.Seqs]
infinite_filter_correct [in OAut.Seqs]
infinite_filter_s_monotone [in OAut.Seqs]
infinite_final_implies_infinite_critical [in OAut.ASStructures]
infinite_merge_at_next_same_color [in OAut.Ramsey]
infinite_merge_at_next [in OAut.Ramsey]
infinite_equiv_indices' [in OAut.Ramsey]
inImages [in FinTypes.FinTypes]
initialW_partitions_in_W [in OAut.Buechi]
initial_r' [in OAut.Complement]
injectiveApply [in FinTypes.BasicDefinitions]
injective_dupfree [in FinTypes.FinTypes]
inr_fix [in FinTypes.Automata]
inr_fix_epsilon [in FinTypes.Automata]
intermediate_infinite [in OAut.NecessityAR]
intersection_incl_intersect [in OAut.Buechi]
intersect_correct [in FinTypes.Automata]
intersect_correct [in OAut.Buechi]
intersect_incl_aut2 [in OAut.Buechi]
intersect_incl_aut1 [in OAut.Buechi]
intersect_acorrect [in OAut.ASStructures]
inter_to_seq_to_inter_correct [in OAut.MSO]
inv_join_separate [in OAut.FinType]
inv_separate_join [in OAut.FinType]
inv_nat_to_pair [in OAut.Ramsey]
in_rem_iff [in FinTypes.External]
in_filter_iff [in FinTypes.External]
in_cons_neq [in FinTypes.External]
in_sing [in FinTypes.External]
in_vP_correct [in OAut.NecessityAR]
in_undup [in FinTypes.FinTypes]
in_lang_prepend [in OAut.Seqs]
ipp [in OAut.Ramsey]
ipp_dm [in OAut.NecessityAR]
irun_final [in OAut.Buechi]
irun_step_final [in OAut.Buechi]
irun_same_states [in OAut.Buechi]
irun_step_to_true [in OAut.Buechi]
irun_initial [in OAut.Buechi]
irun_valid [in OAut.Buechi]
isSuccCorrect [in OAut.AbstractMSO]
isSuccMemCorrect [in OAut.AbstractMSO]
ItoM0Fvar [in OAut.AbstractMSO]
ItoM0Svar [in OAut.AbstractMSO]
ItoM2_fvar_update [in OAut.AbstractMSO]

J

joinASeq_correct_old [in OAut.MSO]
joinASeq_correct_new [in OAut.MSO]
join_snd [in OAut.FinType]
join_fst [in OAut.FinType]

K

kleene_star_correct [in FinTypes.Automata]
kleene_star_correct2 [in FinTypes.Automata]
kleene_delta_ok8 [in FinTypes.Automata]
kleene_delta_ok7 [in FinTypes.Automata]
kleene_delta_ok6 [in FinTypes.Automata]
kleene_star_correct1 [in FinTypes.Automata]
kleene_delta_ok_5 [in FinTypes.Automata]
kleene_delta_ok_4 [in FinTypes.Automata]
kleene_delta_ok_3 [in FinTypes.Automata]
kleene_delta_ok2 [in FinTypes.Automata]
kleene_delta_ok1 [in FinTypes.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 FinTypes.Automata]
lang_omega_iteration_extensional [in OAut.Seqs]
lang_o_iter_extract [in OAut.Seqs]
last_norm_is_final [in OAut.RegularLanguages]
LA_proj_list_equiv_image [in OAut.MSO]
lengthEq [in FinTypes.BasicDefinitions]
leq_correct [in OAut.AbstractMSO]
leq_0 [in OAut.Complement]
less_nfa_correct [in OAut.MSO]
less_implies_accepting [in OAut.MSO]
le_correct [in OAut.AbstractMSO]
le_add [in OAut.Seqs]
le_L_is_le [in OAut.FinType]
Le_K_enum_ok [in OAut.FinType]
list_cc [in FinTypes.External]
list_exists_not_incl [in FinTypes.External]
list_exists_DM [in FinTypes.External]
list_sigma_forall [in FinTypes.External]
list_cycle [in FinTypes.External]
list_eq [in OAut.FinType]
loop [in FinTypes.BasicDefinitions]
loop_admits_ramseyan_fac [in OAut.Ramsey]

M

map_aut_up_correct [in OAut.ASStructures]
max_le [in OAut.BasicDefs]
max_le_right [in OAut.BasicDefs]
max_le_left [in OAut.BasicDefs]
max_of_nat_string_correct [in OAut.Ramsey]
minmso_classic [in OAut.MSO]
minsat_iff_buechi_non_empty [in OAut.MSO]
msatisfies_set_extensional [in OAut.AbstractMSO]
msatisfies_extensional [in OAut.AbstractMSO]
mso_xm_implies_ramsey_fac [in OAut.NecessityAR]
mso_ramseyan_factorization [in OAut.NecessityAR]
mso_DM_exist_neg' [in OAut.AbstractMSO]
mso_DM_exist_neg [in OAut.AbstractMSO]
mso_DM_forall_neg' [in OAut.AbstractMSO]
mso_DM_forall_neg [in OAut.AbstractMSO]
mso_DM_ex2 [in OAut.AbstractMSO]
mso_DM_ex1 [in OAut.AbstractMSO]
mso_DM_finBigAND' [in OAut.AbstractMSO]
mso_DM_finBigAND [in OAut.AbstractMSO]
mso_DM_finBigOR' [in OAut.AbstractMSO]
mso_DM_finBigOR [in OAut.AbstractMSO]
mso_DM_impl [in OAut.AbstractMSO]
mso_DM_neg_and' [in OAut.AbstractMSO]
mso_DM_neg_and [in OAut.AbstractMSO]
mso_DM_neg_or [in OAut.AbstractMSO]
mso_DN [in OAut.AbstractMSO]
mso_xm_satisfies [in OAut.AbstractMSO]
mso_coincidence_bi [in OAut.AbstractMSO]
mso_coincidence' [in OAut.AbstractMSO]
mso_coincidence [in OAut.AbstractMSO]
mso_classic [in OAut.MSO]
mul_div [in OAut.BasicDefs]
mul_geq_left [in OAut.BasicDefs]
mul_ge_0_reverse [in OAut.BasicDefs]
mul_ge_0 [in OAut.BasicDefs]
mul_yields_idempotent [in OAut.Ramsey]
mul_mult [in OAut.Ramsey]
mul_distr [in OAut.Ramsey]
mul_comm [in OAut.Ramsey]
mul_step [in OAut.Ramsey]

N

narrowVectorCorrect [in OAut.FinType]
narrow_to_free_vars [in OAut.MSO]
nat_partition_extensional [in OAut.MSO]
nat_equation_1 [in OAut.Seqs]
nat_pair_le_not_equal [in OAut.Seqs]
nat_to_pair_halfspace [in OAut.Ramsey]
negOr [in FinTypes.BasicDefinitions]
next_position_exists_all [in OAut.Seqs]
next_position_exists_correct [in OAut.Seqs]
next_position_exists_increasing [in OAut.Seqs]
next_position_all [in OAut.Seqs]
next_position_bounds [in OAut.Seqs]
next_position_correct [in OAut.Seqs]
nfa_string_lang_cc [in OAut.RegularLanguages]
nfa_omega_iter_correct [in OAut.Buechi]
nfa_omega_iter'_correct [in OAut.Buechi]
nfa_omega_iter'_accepts_aut [in OAut.Buechi]
nil_kleene [in FinTypes.Automata]
NoneElement [in FinTypes.FinTypes]
normalize_is_normalized [in OAut.RegularLanguages]
normalize_correct [in OAut.RegularLanguages]
normalize_accepts_aut [in OAut.RegularLanguages]
notInMapCons [in FinTypes.FinTypes]
notInZero [in FinTypes.BasicDefinitions]
not_in_cons [in FinTypes.External]
not_finite_implies_infinite [in OAut.NecessityAR]
not_finite_intermediate [in OAut.NecessityAR]
not_empty_correct [in OAut.AbstractMSO]
not_part_of_complement_implies_aut [in OAut.ASStructures]
not_tilde_w_equiv_sym [in OAut.Ramsey]
NullMul [in FinTypes.BasicDefinitions]
nums_leq_K_length [in OAut.FinType]
nums_leq_K_dupfree [in OAut.FinType]
nums_leq_K_complete [in OAut.FinType]

O

omega_iteration_final [in OAut.Buechi]
omega_iteration_infiniteP [in OAut.Seqs]
omega_iter_unfold [in OAut.Seqs]
omega_iter_first_new [in OAut.Seqs]
omega_iter_first [in OAut.Seqs]
omega_iteration_extensional [in OAut.Seqs]
omega_iteration_valid_run [in OAut.ASStructures]
onestate_correct [in FinTypes.Automata]
Option_Card [in FinTypes.FinTypes]
option_enum_ok [in FinTypes.FinTypes]
or_correct [in OAut.AbstractMSO]
os_nfa_correct [in OAut.RegularLanguages]
os_nfa_only_accepts_v [in OAut.RegularLanguages]
os_nfa_accepts_v [in OAut.RegularLanguages]
other_norm_is_aut_state [in OAut.RegularLanguages]

P

pair_proj2 [in OAut.BasicDefs]
pair_proj1 [in OAut.BasicDefs]
pair_nat_choice [in OAut.Ramsey]
partition_run_on_concat_inf [in OAut.Buechi]
partition_run_on_prepend_string [in OAut.Buechi]
partition_correct [in OAut.MSO]
part_of_complement_implies_complement [in OAut.ASStructures]
path_length_bounded [in OAut.NFAs]
path_extensional [in OAut.NFAs]
periodic_run_matching_pseq_size [in OAut.ASStructures]
periodic_run [in OAut.ASStructures]
pick [in FinTypes.FinTypes]
pidgeonHole_bij [in FinTypes.FinTypes]
pidgeonHole_surj [in FinTypes.FinTypes]
pidgeonHole_inj [in FinTypes.FinTypes]
power_extensional [in FinTypes.External]
power_nil [in FinTypes.External]
power_incl [in FinTypes.External]
pow_ge_zero [in OAut.BasicDefs]
pow_ge_zero' [in OAut.BasicDefs]
prefix_admits_ramseyan_fac [in OAut.Ramsey]
preimage_aut_correct [in OAut.Buechi]
preimage_aut_acorrect [in OAut.ASStructures]
prepend_step_valid_path [in OAut.NFAs]
prepend_nfa_correct [in OAut.Buechi]
prepend_nfa'_correct [in OAut.Buechi]
prepend_aut_accepts_prepend_omega [in OAut.Buechi]
prepend_aut_is_prepend_omega [in OAut.Buechi]
prepend_on_omega_iteration [in OAut.Seqs]
prepend_string_rest'' [in OAut.Seqs]
prepend_string_rest' [in OAut.Seqs]
prepend_string_rest [in OAut.Seqs]
prepend_string_begin [in OAut.Seqs]
prepend_prefix_begin [in OAut.Seqs]
prepend_prefix_rest' [in OAut.Seqs]
prepend_prefix_rest2 [in OAut.Seqs]
prepend_prefix_rest [in OAut.Seqs]
prepend_rest2 [in OAut.Seqs]
prepend_rest [in OAut.Seqs]
prepend_first [in OAut.Seqs]
prepend_string_valid_run [in OAut.ASStructures]
preservation_FCIter [in FinTypes.FinTypes]
preservation_iter [in FinTypes.FinTypes]
preservation_step [in FinTypes.FinTypes]
ProdCount [in FinTypes.FinTypes]
Prod_Card [in FinTypes.FinTypes]
prod_enum_ok [in FinTypes.FinTypes]
prod_correct [in FinTypes.Automata]
prod_delta_star [in FinTypes.Automata]
prod_nil [in FinTypes.BasicDefinitions]
projection_list_aclosed [in OAut.MSO]
proj1_sig_fun [in FinTypes.BasicDefinitions]
proveOne [in FinTypes.FinTypes]
pure_eq [in FinTypes.BasicDefinitions]
pure_impure [in FinTypes.BasicDefinitions]
pure_equiv [in FinTypes.BasicDefinitions]
pure_le_k_iff [in OAut.FinType]
purify [in FinTypes.BasicDefinitions]

R

ramseyan_factorization [in OAut.Ramsey]
RamseyFacFromComplement [in OAut.NecessityAR]
RamseyFacImpliesMarkov [in OAut.Ramsey]
RamseyFac_iff_AdditiveRamsey [in OAut.Ramsey]
ramseyTotality [in OAut.Complement]
ramsey_nfa_correct [in OAut.NecessityAR]
ramsey_idem_aut_correct [in OAut.NecessityAR]
ramsey_idem_aut'_scorrect [in OAut.NecessityAR]
ramsey_idem_aut'_run_is_inl [in OAut.NecessityAR]
reachable_transitive [in FinTypes.Automata]
reachable_with_reachable [in FinTypes.Automata]
reach_reachable_with [in FinTypes.Automata]
reach_correct [in FinTypes.Automata]
reach_correct2 [in FinTypes.Automata]
reach_correct2' [in FinTypes.Automata]
reach_correct1 [in FinTypes.Automata]
reach_least_fp [in FinTypes.Automata]
rem_inclr [in FinTypes.External]
rem_reorder [in FinTypes.External]
rem_id [in FinTypes.External]
rem_fst' [in FinTypes.External]
rem_fst [in FinTypes.External]
rem_comm [in FinTypes.External]
rem_equi [in FinTypes.External]
rem_app' [in FinTypes.External]
rem_app [in FinTypes.External]
rem_neq [in FinTypes.External]
rem_in [in FinTypes.External]
rem_cons' [in FinTypes.External]
rem_cons [in FinTypes.External]
rem_mono [in FinTypes.External]
rem_incl [in FinTypes.External]
rem_not_in [in FinTypes.External]
rem_loops_preserves_ends [in OAut.NFAs]
rem_loops'_preserves_ends [in OAut.NFAs]
rem_loops_length [in OAut.NFAs]
rem_loops'_length [in OAut.NFAs]
rem_loops_valid [in OAut.NFAs]
rem_loops'_valid [in OAut.NFAs]
rem_not_in_eq [in OAut.FinType]
rem_sub [in OAut.FinType]
rep_dupfree [in FinTypes.External]
rep_idempotent [in FinTypes.External]
rep_injective [in FinTypes.External]
rep_eq [in FinTypes.External]
rep_eq' [in FinTypes.External]
rep_mono [in FinTypes.External]
rep_equi [in FinTypes.External]
rep_in [in FinTypes.External]
rep_incl [in FinTypes.External]
rep_power [in FinTypes.External]
revert_concat_second [in OAut.Seqs]
revert_concat_first [in OAut.Seqs]
revert_drop [in OAut.Seqs]
revert_prepend_string [in OAut.Seqs]
rightResult [in FinTypes.FinTypes]
run_for_transforms_correct [in OAut.Complement]
R'k0_eq_Rk0 [in OAut.Complement]

S

safe_dclosed [in OAut.BasicDefs]
sat_iff_minsat [in OAut.AbstractMSO]
sat_fromMinMSO_s_update [in OAut.AbstractMSO]
sat_fromMinMSO_update [in OAut.AbstractMSO]
sat_fromMinMSO [in OAut.AbstractMSO]
sat_iff_buechi_non_empty [in OAut.MSO]
sclosure_complement [in OAut.RegularLanguages]
sclosure_diff [in OAut.RegularLanguages]
sclosure_intersection [in OAut.RegularLanguages]
sclosure_union [in OAut.RegularLanguages]
scomplement_correct [in OAut.RegularLanguages]
sdiff_correct [in OAut.RegularLanguages]
second_order_interpretation [in OAut.AbstractMSO]
second_order_var_singleton [in OAut.AbstractMSO]
separate_unchanged [in OAut.FinType]
seqToInterGetX [in OAut.MSO]
seqToInterGetY [in OAut.MSO]
seqToSetCorrect [in OAut.MSO]
seqToSetCover [in OAut.MSO]
seqToSetPartition [in OAut.MSO]
seqToSetUnique [in OAut.MSO]
seq_implies_final_loop [in OAut.Buechi]
seq_in_empty_aut_contradicts [in OAut.Buechi]
setToSeqCorrect [in OAut.MSO]
setToSeqExtensional [in OAut.MSO]
setToSeqExtensional2 [in OAut.MSO]
setToSeqParitionCorrect [in OAut.MSO]
setToSeqParitionCorrectInv [in OAut.MSO]
set_equivalent_iff_seq_extensional [in OAut.MSO]
sigT_enum_ok [in FinTypes.FinTypes]
sigT_proj2_fun [in FinTypes.BasicDefinitions]
sigT_proj1_fun [in FinTypes.BasicDefinitions]
Sig_reach [in FinTypes.Automata]
singleton_interpretation [in OAut.AbstractMSO]
singleton_correct2 [in OAut.AbstractMSO]
singleton_correct [in OAut.AbstractMSO]
sing_equiv [in OAut.AbstractMSO]
sintersect_correct [in OAut.RegularLanguages]
size_induction [in FinTypes.External]
slanguage_extensional [in OAut.RegularLanguages]
slot_in_smonotone [in OAut.Ramsey]
SomeElement [in FinTypes.FinTypes]
split_path [in OAut.NFAs]
split_final_transforms [in OAut.Complement]
split_transforms [in OAut.Complement]
split_position_lang_prepend [in OAut.Seqs]
split_string_eq [in OAut.Seqs]
split_critical_index_begin [in OAut.ASStructures]
states_do_not_mix [in OAut.Buechi]
step_consistent_least_fp [in FinTypes.FinTypes]
step_trans_fp_incl [in FinTypes.FinTypes]
step_iter_consistent [in FinTypes.FinTypes]
step_reach_consistent [in FinTypes.Automata]
Streicher_K [in FinTypes.BasicDefinitions]
strings_equal_transitive [in OAut.Seqs]
strings_equal_symmetric [in OAut.Seqs]
strings_equal_reflexive [in OAut.Seqs]
string_final_R' [in OAut.Complement]
string_omega_omega_iteration [in OAut.Seqs]
string_zip_snd_up [in OAut.Seqs]
string_zip_fst_up [in OAut.Seqs]
subType_enum_ok [in FinTypes.FinTypes]
subtype_extensionality [in FinTypes.BasicDefinitions]
SumCard [in FinTypes.FinTypes]
sum_enum_ok [in FinTypes.FinTypes]
sum_ramseyan_fac [in OAut.Ramsey]
sunion_correct [in OAut.RegularLanguages]
supdate_preserves_singleton [in OAut.AbstractMSO]
surjectiveApply [in FinTypes.BasicDefinitions]
surj_sub [in FinTypes.FinTypes]
switch_from_V_to_W [in OAut.Buechi]
s_s'_pair_aut_correct [in OAut.Complement]
s_monotone_begin_in [in OAut.Seqs]
s_monotone_drop [in OAut.Seqs]
s_monotone_ge_zero' [in OAut.Seqs]
s_monotone_ge_zero [in OAut.Seqs]
s_monotone_order_preserving_backwards [in OAut.Seqs]
s_monotone_order_preserving [in OAut.Seqs]
s_monotone_strict_order_preserving [in OAut.Seqs]
s_monotone_strict_order_preserving' [in OAut.Seqs]
s_monotone_ge [in OAut.Seqs]
s_monotone_unbouded [in OAut.Seqs]
s_monotone_unbouded_ge [in OAut.Seqs]
s_monotone_id [in OAut.Seqs]
S_z_minus_1 [in OAut.BasicDefs]

T

test [in OAut.ASStructures]
tff_recognizes_transforms_final [in OAut.Complement]
tff_is_transforms_final [in OAut.Complement]
tff_accepts_tranforms_final [in OAut.Complement]
tf_recognizes_transforms [in OAut.Complement]
tf_is_transforms [in OAut.Complement]
tf_accepts_tranforms [in OAut.Complement]
tilde_w_equiv_mso_correct [in OAut.NecessityAR]
tilde_congruence [in OAut.Complement]
tilde_w_equiv_cc_nat [in OAut.Ramsey]
tilde_w_equiv_finite_index [in OAut.Ramsey]
tilde_w_index_transitive [in OAut.Ramsey]
tilde_w_index_symmetric [in OAut.Ramsey]
tilde_w_index_reflexive [in OAut.Ramsey]
tilde_w_extend [in OAut.Ramsey]
toDFA_correct [in FinTypes.Automata]
toDFA_delta_star_correct2 [in FinTypes.Automata]
toDFA_delta_star_correct1 [in FinTypes.Automata]
toDFA_delta_correct [in FinTypes.Automata]
toeqTypeCorrect [in FinTypes.BasicDefinitions]
toeqTypeCorrect_sub [in FinTypes.BasicDefinitions]
toeqTypeCorrect_sigT [in FinTypes.BasicDefinitions]
toeqTypeCorrect_list [in FinTypes.BasicDefinitions]
toeqTypeCorrect_true [in FinTypes.BasicDefinitions]
toeqTypeCorrect_false [in FinTypes.BasicDefinitions]
toeqTypeCorrect_empty [in FinTypes.BasicDefinitions]
toeqTypeCorrect_prod [in FinTypes.BasicDefinitions]
toeqTypeCorrect_option [in FinTypes.BasicDefinitions]
toeqTypeCorrect_nat [in FinTypes.BasicDefinitions]
toeqTypeCorrect_bool [in FinTypes.BasicDefinitions]
toeqTypeCorrect_unit [in FinTypes.BasicDefinitions]
toeqType_idempotent [in FinTypes.BasicDefinitions]
toeqType_sum [in FinTypes.BasicDefinitions]
toFinTypeFromListEq [in OAut.FinType]
tofinType_sub_correct [in FinTypes.FinTypes]
tofinType_sigT_correct [in FinTypes.FinTypes]
tofinType_vector_correct [in FinTypes.FinTypes]
tofinType_idempotent [in FinTypes.FinTypes]
tofinType_works [in FinTypes.FinTypes]
toNFA_correct [in FinTypes.Automata]
toNFA_delta_star_correct [in FinTypes.Automata]
top_correct [in OAut.AbstractMSO]
toSigTList_count [in FinTypes.FinTypes]
toSubList_count [in FinTypes.FinTypes]
toSumList1_missing [in FinTypes.BasicDefinitions]
toSumList1_count [in FinTypes.BasicDefinitions]
toSumList2_missing [in FinTypes.BasicDefinitions]
toSumList2_count [in FinTypes.BasicDefinitions]
toV1Different [in OAut.AbstractMSO]
toV1Double [in OAut.AbstractMSO]
toV1Injective [in OAut.AbstractMSO]
toV1_even [in OAut.AbstractMSO]
toV2Different [in OAut.AbstractMSO]
toV2Double [in OAut.AbstractMSO]
toV2Injective [in OAut.AbstractMSO]
toV2_not_even [in OAut.AbstractMSO]
to_ind_nfa_correct [in OAut.RegularLanguages]
to_min_mso_complete [in OAut.AbstractMSO]
to_min_mso_sings [in OAut.AbstractMSO]
to_min_mso_correct [in OAut.AbstractMSO]
to_seq_unchanged' [in OAut.Seqs]
to_seq_unchanged [in OAut.Seqs]
to_bounded_unchanged [in OAut.Seqs]
True_enum_ok [in FinTypes.FinTypes]

U

undup_idempotent [in FinTypes.External]
undup_id [in FinTypes.External]
undup_equi [in FinTypes.External]
undup_incl [in FinTypes.External]
undup_id_equi [in FinTypes.External]
union_correct [in OAut.Buechi]
union_symmetric [in OAut.Buechi]
union_symmetric_acc [in OAut.Buechi]
union_acorrect [in OAut.ASStructures]
unique_correct [in OAut.MSO]
unit_enum_ok [in FinTypes.FinTypes]
univ_aut_scorrect [in OAut.RegularLanguages]
univ_aut_correct [in OAut.Buechi]
up_eq_compl [in OAut.NecessityAR]
up_equiv_iff_omega_equiv [in OAut.MSO]
up_sat_iff_omega_sat [in OAut.MSO]
up_buechi_nonempty_iff_buechi_nonempty [in OAut.MSO]
up_zip_correct [in OAut.Seqs]
up_zip_proj2 [in OAut.Seqs]
up_zip_proj1 [in OAut.Seqs]
up_zip''_proj2 [in OAut.Seqs]
up_zip''_proj1 [in OAut.Seqs]
up_zip'_prefix_length [in OAut.Seqs]
up_zip'_equiv [in OAut.Seqs]
up_loop [in OAut.Seqs]
up_prefix [in OAut.Seqs]
up_map_correct [in OAut.Seqs]
up_admits_ramseyan_fac [in OAut.Ramsey]
U_correct [in FinTypes.Automata]

V

valid_path_reachable [in OAut.NFAs]
valid_run_reachable [in OAut.NFAs]
valid_path_cut [in OAut.NFAs]
valid_prepend_path [in OAut.NFAs]
valid_prepend_path' [in OAut.NFAs]
valid_concat_paths [in OAut.NFAs]
valid_path_is_path_everywhere [in OAut.NFAs]
valid_run_is_path_everywhere [in OAut.NFAs]
valid_path_drop [in OAut.NFAs]
valid_run_drop [in OAut.NFAs]
valid_path_decrease [in OAut.NFAs]
valid_path_decrease' [in OAut.NFAs]
valid_run_is_path_from_begin [in OAut.NFAs]
valid_path_extensional [in OAut.NFAs]
valid_run_extensional [in OAut.NFAs]
valid_r' [in OAut.Complement]
valid_periodic_run [in OAut.ASStructures]
valid_path_prepended_string [in OAut.ASStructures]
vars_for_elems_bound [in OAut.NecessityAR]
vars_for_elems_injective [in OAut.NecessityAR]
vars_for_list_injective [in OAut.NecessityAR]
vars_for_list_bound [in OAut.NecessityAR]
vars_for_list_ge [in OAut.NecessityAR]
vectorise_apply_inverse [in FinTypes.FinTypes]
vectorise_apply_inverse' [in FinTypes.FinTypes]
Vector_Card [in FinTypes.FinTypes]
vector_extensionality [in FinTypes.FinTypes]
vector_enum_ok [in FinTypes.FinTypes]
vector_eq [in OAut.FinType]
vv_omega_unfold [in OAut.Seqs]
VW_aut_correct [in OAut.Complement]
vX_vP_disjoint [in OAut.NecessityAR]
v_transforms [in OAut.Complement]
v'_transforms [in OAut.Complement]

W

wrap_string [in OAut.Seqs]
W_transforms [in OAut.Complement]
W_final_iff [in OAut.Complement]
W'_transforms [in OAut.Complement]

X

XinA [in OAut.MSO]
xm_word_problem [in OAut.ASStructures]
XM_implies_RamseyFac [in OAut.Ramsey]

Y

YinA [in OAut.MSO]

Z

zeroElCorrect [in OAut.AbstractMSO]
zip_existential [in OAut.MSO]

Constructor Index

A

And [in OAut.AbstractMSO]

D

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

E

EqType [in FinTypes.External]

F

FEx [in OAut.AbstractMSO]
FinType [in FinTypes.FinTypes]
FinTypeC [in FinTypes.FinTypes]

I

Incl [in OAut.AbstractMSO]

L

Le [in OAut.AbstractMSO]

M

MAnd [in OAut.AbstractMSO]
Mem [in OAut.AbstractMSO]
MEx [in OAut.AbstractMSO]
MIncl [in OAut.AbstractMSO]
mkAdmissibleSequenceStructure [in OAut.ASStructures]
mkNatSet [in OAut.AbstractMSO]
mknfa [in OAut.NFAs]
mkSequenceStructure [in OAut.ASStructures]
mkSG [in OAut.Ramsey]
mkstring [in OAut.Seqs]
mkUPSeq [in OAut.Seqs]
MLe [in OAut.AbstractMSO]
MNeg [in OAut.AbstractMSO]

N

Neg [in OAut.AbstractMSO]
NFA [in FinTypes.Automata]

R

refl [in FinTypes.Automata]

S

safeB [in OAut.BasicDefs]
safeS [in OAut.BasicDefs]
SEx [in OAut.AbstractMSO]
step [in FinTypes.Automata]

Inductive Index

D

dupfree [in FinTypes.External]

F

Form [in OAut.AbstractMSO]
FormMin [in OAut.AbstractMSO]

R

reachable [in FinTypes.Automata]

S

safe [in OAut.BasicDefs]

Projection Index

A

add [in OAut.Ramsey]
amap [in OAut.ASStructures]
amap_correct [in OAut.ASStructures]
ASeq [in OAut.ASStructures]
aseq_run [in OAut.ASStructures]
aseq_to_seq [in OAut.ASStructures]
Assoc [in OAut.Ramsey]
azip [in OAut.ASStructures]
azip_correct [in OAut.ASStructures]

C

CC [in OAut.ASStructures]
class [in FinTypes.FinTypes]

D

decide_rel [in FinTypes.External]
decide_pred [in FinTypes.External]
decide_eq [in FinTypes.External]
decMemSet [in OAut.AbstractMSO]
dec_alanguage_empty_informative [in OAut.ASStructures]
delta_Q [in FinTypes.Automata]
delta_S [in FinTypes.Automata]

E

elements [in OAut.Ramsey]
enum [in FinTypes.FinTypes]
enum_ok [in FinTypes.FinTypes]
eqtype [in FinTypes.External]
exact_at_correct [in OAut.ASStructures]
exact_at [in OAut.ASStructures]

F

F [in FinTypes.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]
loop [in OAut.Seqs]

M

map_aut_acorrect [in OAut.ASStructures]
memSet [in OAut.AbstractMSO]

N

NatSet [in OAut.AbstractMSO]

P

predicate [in FinTypes.External]
prefix [in OAut.Seqs]

Q

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

R

relation [in FinTypes.External]

S

s [in FinTypes.Automata]
S [in FinTypes.Automata]
seq [in OAut.Seqs]
singletonSet [in OAut.AbstractMSO]
singletonSetCorrect1 [in OAut.AbstractMSO]
singletonSetCorrect2 [in OAut.AbstractMSO]
state [in OAut.NFAs]

T

totality [in OAut.ASStructures]
transition [in OAut.NFAs]
transition_dec [in OAut.NFAs]
type [in FinTypes.FinTypes]

Section Index

A

AdditiveRamsey [in OAut.Ramsey]

B

BigZip [in OAut.ASStructures]
BuechiAutomaton [in OAut.Buechi]
BuechiEquivalenceRelation [in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable [in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsFinalRecognizable [in OAut.Complement]
BuechiEquivalenceRelation.BuechiEqivalenceClassRecognizable.TransformsRecognizable [in OAut.Complement]
BuechiEquivalenceRelation.BuechiEquivalenceClassRecognizableMyhillNerode [in OAut.Complement]
BuechiEquivalenceRelation.Compatibility [in OAut.Complement]
BuechiEquivalenceRelation.Totality [in OAut.Complement]

C

Cardinality [in FinTypes.External]
ClassicalReasoning [in OAut.AbstractMSO]
ClosureProperties [in OAut.RegularLanguages]
ClosureProperties [in OAut.ASStructures]
ClosureProperties.Complement [in OAut.ASStructures]
ClosureProperties.ComplementCorollaries [in OAut.ASStructures]
ClosureUnderComplementImpliesAdditiveRamsey [in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.RamseyNFA [in OAut.NecessityAR]
ClosureUnderComplementImpliesAdditiveRamsey.RamseyNFA.RamseyNFAIdem [in OAut.NecessityAR]
Complement [in OAut.Complement]
ConcatInfPrependNFA [in OAut.Buechi]
ConvertToNFA [in OAut.RegularLanguages]

D

DecBuechiAutomatonEmpty [in OAut.Buechi]
DecConnected [in OAut.NFAs]
DeriveRamseyFac [in OAut.Ramsey]
DeriveRamseyFac.ConstructiveChoiceNcrossN [in OAut.Ramsey]
DFA [in FinTypes.Automata]
DFA.Operations [in FinTypes.Automata]
DFA.Operations.Product_automaton [in FinTypes.Automata]
DFA.Reachability [in FinTypes.Automata]
Dupfree [in FinTypes.External]
DupFreeDis [in FinTypes.External]

E

EmptyBuechiAutomaton [in OAut.Buechi]
Equi [in FinTypes.External]

F

FilterLemmas [in FinTypes.External]
FilterLemmas_pq [in FinTypes.External]
FindNextPosition [in OAut.Seqs]
FindNextPosition.NextPosition [in OAut.Seqs]
FindNextPosition.NextPositionExists [in OAut.Seqs]
FiniteClosureIteration [in FinTypes.FinTypes]
FiniteIterationOfString [in OAut.Seqs]
FiniteSemiGroup [in OAut.Ramsey]
First [in OAut.BasicDefs]
FirstKFinType [in OAut.FinType]
Fixedpoints [in FinTypes.FinTypes]

I

ImageNFA [in OAut.Buechi]
Inclusion [in FinTypes.External]
Infinite [in OAut.Seqs]
InfiniteConcat [in OAut.Seqs]
InfiniteFilter [in OAut.Seqs]
IntersectionClosure [in OAut.Buechi]
IntersectionClosure.IRun [in OAut.Buechi]

L

LanguageLemmata [in OAut.BasicDefs]
LanguageOmegaIteration [in OAut.Seqs]
Languages [in OAut.BasicDefs]
ListProjection [in OAut.MSO]

M

Membership [in FinTypes.External]
MSO [in OAut.AbstractMSO]
MSOClassicalImpliesRamseyFac [in OAut.NecessityAR]
MSOClassicalImpliesRamseyFac.ADD_Formula [in OAut.NecessityAR]
MSOtoBuechi [in OAut.MSO]
MSOtoBuechi.BaseNFAs [in OAut.MSO]
MSOtoBuechi.BaseNFAs.InclusionNFA [in OAut.MSO]
MSOtoBuechi.BaseNFAs.LessNFA [in OAut.MSO]
MSO.ReducablityOfFirstOrderVariables [in OAut.AbstractMSO]
MSO.SyntacticSugarFirstOrder [in OAut.AbstractMSO]

N

NFAOmegaIteration [in OAut.Buechi]
NFAOmegaIteration.OmegaIterNormalized [in OAut.Buechi]
NFAStringLanguage [in OAut.RegularLanguages]
NormalizeNFA [in OAut.RegularLanguages]

O

OmegaIteration [in OAut.Seqs]
OneStringNFA [in OAut.RegularLanguages]

P

Partition [in OAut.MSO]
PowerRep [in FinTypes.External]
PreImageNFA [in OAut.Buechi]
PrependNFA [in OAut.Buechi]
PrependNFA.PrependNormalizedNFA [in OAut.Buechi]

Q

Quotients [in OAut.FinType]

R

RamseyanFactorizationMarkov [in OAut.Ramsey]
Removal [in FinTypes.External]

S

SeqOperations [in OAut.Seqs]
Sets [in OAut.AbstractMSO]
SpecialSeqOperations [in OAut.MSO]
StrictlyMonotoneSeqs [in OAut.Seqs]
StringOperationLemmas [in OAut.Seqs]
StringOperations [in OAut.Seqs]
StringsEq [in OAut.Seqs]
StringsOfConstantLength [in OAut.Seqs]

T

Test [in FinTypes.FinTypes]
TransitionGraph [in OAut.NFAs]
TransitionGraph.InfConcat [in OAut.NFAs]

U

UltimatelyPeriodicSequences [in OAut.Seqs]
UltimatelyPeriodicSequences.Basic [in OAut.Seqs]
UltimatelyPeriodicSequences.StringZip [in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip [in OAut.Seqs]
UltimatelyPeriodicSequences.UPZip'' [in OAut.Seqs]
Undup [in FinTypes.External]
UnionClosure [in OAut.Buechi]
UnionClosure.Def [in OAut.Buechi]
UniversalBuechiAutomaton [in OAut.Buechi]
UPAdmissible [in OAut.ASStructures]
UPAdmissible.PeriodicRun [in OAut.ASStructures]

V

Vectors [in OAut.FinType]
Vectors.ConvertRemNotIn [in OAut.FinType]
Vectors.Narrowing [in OAut.FinType]

X

XMWordProblemImpliesInfinitePigeonholePrinciple [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AllNotNFA [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.AtLeastOneNFA [in OAut.NecessityAR]
XMWordProblemImpliesInfinitePigeonholePrinciple.FiniteAut [in OAut.NecessityAR]

Instance Index

A

accepting_proper [in OAut.Buechi]
accept_dec [in FinTypes.Automata]
acc_dec [in FinTypes.Automata]
ADD_Proper [in OAut.Ramsey]
amap_proper [in OAut.ASStructures]
and_dec [in FinTypes.External]
app_equi_proper [in FinTypes.External]
app_incl_proper [in FinTypes.External]
aseq_equal_equiv [in OAut.ASStructures]

B

bool_eq_dec [in FinTypes.External]
bounded_strict_forall [in OAut.FinType]
bounded_exist [in OAut.FinType]
bounded_forall [in OAut.FinType]
bounded_type_exist [in OAut.FinType]
buechi_language_proper [in OAut.Buechi]
buechi_eq_class_proper [in OAut.Complement]

C

cancat_strings_proper [in OAut.Seqs]
card_equi_proper [in FinTypes.External]
conact_delta_dec [in FinTypes.Automata]
cons_equi_proper [in FinTypes.External]
cons_incl_proper [in FinTypes.External]

D

decActivW [in OAut.Buechi]
decMemSetInstance [in OAut.AbstractMSO]
decp_dec [in FinTypes.External]
decRel_dec [in FinTypes.External]
dec_norm_transition [in OAut.RegularLanguages]
dec_saccepting [in OAut.RegularLanguages]
dec_sfinal [in OAut.RegularLanguages]
dec_sinitial [in OAut.RegularLanguages]
dec_svalid [in OAut.RegularLanguages]
dec_transition_all [in OAut.NecessityAR]
dec_transition_at_least_one [in OAut.NecessityAR]
dec_ramset_transition [in OAut.NecessityAR]
dec_connected [in OAut.NFAs]
dec_valid_path [in OAut.NFAs]
dec_even [in OAut.AbstractMSO]
dec_prepend_state_final [in OAut.Buechi]
dec_prepend_transition [in OAut.Buechi]
dec_intersection_transition [in OAut.Buechi]
dec_intersection_final [in OAut.Buechi]
dec_intersection_initial [in OAut.Buechi]
dec_union_final [in OAut.Buechi]
dec_union_initial [in OAut.Buechi]
dec_union_transition [in OAut.Buechi]
dec_VW_part_of_complement [in OAut.Complement]
dec_pure_W_final [in OAut.Complement]
dec_buechi_eq_class [in OAut.Complement]
dec_transforms_final [in OAut.Complement]
dec_transforms [in OAut.Complement]
dec_pair_eq [in OAut.MSO]
dec_less_transition [in OAut.MSO]
dec_incl_transition [in OAut.MSO]
dec_ciritcal_index [in OAut.ASStructures]
dec_critical_index_unfold [in OAut.ASStructures]
dec_smallest [in OAut.FinType]
dec_pure_le_k_public [in OAut.FinType]
dec_pure_le_k [in OAut.FinType]
dec_le_k [in OAut.FinType]
dec_merge_at [in OAut.Ramsey]
delta_Q_star_dec [in FinTypes.Automata]
dev_prepend_state_initial [in OAut.Buechi]
drop_proper [in OAut.Seqs]

E

EisEquivProper [in OAut.FinType]
empty_dec [in FinTypes.Automata]
Empty_set_eq_dec [in FinTypes.BasicDefinitions]
equivalence_class_extensional_proper [in OAut.Complement]
equivalence_class_closed_proper [in OAut.Complement]
equiv_eq_dec [in FinTypes.Automata]
equi_Equivalence [in FinTypes.External]
eq_dec_sigT [in FinTypes.BasicDefinitions]
exists_not_accept_dec [in FinTypes.Automata]
exists_accept_dec [in FinTypes.Automata]
extract_proper [in OAut.Seqs]

F

False_dec [in FinTypes.External]
False_eq_dec [in FinTypes.BasicDefinitions]
final_dec_public [in OAut.NFAs]
FinTypeClass2 [in FinTypes.FinTypes]
finTypeC_sub [in FinTypes.FinTypes]
finTypeC_sigT [in FinTypes.FinTypes]
finTypeC_vector [in FinTypes.FinTypes]
finTypeC_sum [in FinTypes.FinTypes]
finTypeC_Option [in FinTypes.FinTypes]
finTypeC_Prod [in FinTypes.FinTypes]
finTypeC_False [in FinTypes.FinTypes]
finTypeC_True [in FinTypes.FinTypes]
finTypeC_empty [in FinTypes.FinTypes]
finTypeC_unit [in FinTypes.FinTypes]
finTypeC_bool [in FinTypes.FinTypes]
finTypeC_Le_K [in OAut.FinType]
finType_exists_dec [in FinTypes.FinTypes]
finType_forall_dec [in FinTypes.FinTypes]
fromListC [in FinTypes.FinTypes]
f_weak_coincidence [in OAut.AbstractMSO]

I

iff_dec [in FinTypes.External]
impl_dec [in FinTypes.External]
incl_equi_proper [in FinTypes.External]
incl_preorder [in FinTypes.External]
infiniteP_proper [in OAut.Seqs]
initial_dec_public [in OAut.NFAs]
in_equi_proper [in FinTypes.External]
in_incl_proper [in FinTypes.External]

K

kleene_delta_dec [in FinTypes.Automata]
kleene_acc_dec [in FinTypes.Automata]

L

language_complement_proper [in OAut.BasicDefs]
language_difference_proper [in OAut.BasicDefs]
language_intersection_proper [in OAut.BasicDefs]
language_union_proper [in OAut.BasicDefs]
language_eq_mem [in OAut.BasicDefs]
language_eq_equivalence [in OAut.BasicDefs]
lang_sub_dec [in FinTypes.Automata]
lang_prepend_proper [in OAut.Seqs]
lang_omega_iteration_proper [in OAut.Seqs]
LE_K_eq_dec [in OAut.FinType]
list_exists_dec [in FinTypes.External]
list_forall_dec [in FinTypes.External]
list_in_dec [in FinTypes.External]
list_eq_dec [in FinTypes.External]
logic_dec_satis [in OAut.NecessityAR]

M

memSet_proper [in OAut.AbstractMSO]

N

NatSetFromSeq [in OAut.MSO]
nat_le_dec [in FinTypes.External]
nat_eq_dec [in FinTypes.External]
not_dec [in FinTypes.External]

O

OmegaNatSet [in OAut.NecessityAR]
omega_classic [in OAut.MSO]
omega_iteration_proper_index [in OAut.Seqs]
omega_iteration_proper [in OAut.Seqs]
option_eq_dec [in FinTypes.BasicDefinitions]
or_dec [in FinTypes.External]

P

path_proper [in OAut.NFAs]
predCons_dec [in FinTypes.Automata]
prepend_string_proper_index [in OAut.Seqs]
prepend_string_proper [in OAut.Seqs]
prod_pred_dec [in FinTypes.Automata]
prod_eq_dec [in FinTypes.BasicDefinitions]

R

reachable_with_something_dec [in FinTypes.Automata]
reachable_dec [in FinTypes.Automata]

S

seq_eq_index [in OAut.Seqs]
seq_map_proper [in OAut.Seqs]
seq_zip_proper [in OAut.Seqs]
seq_equal_Equivalence [in OAut.Seqs]
seq_dec_exists_bounded [in OAut.ASStructures]
set_equiv_Equivalence [in OAut.AbstractMSO]
Sig_dec [in FinTypes.Automata]
SInter_ext_equiv [in OAut.AbstractMSO]
strict_bounded_exist [in OAut.FinType]
strings_equal_Equivalence [in OAut.Seqs]
string_lastindex_proper [in OAut.Seqs]
subset_proper [in OAut.AbstractMSO]
subType_eq_dec [in FinTypes.BasicDefinitions]
sum_eq_dec [in FinTypes.BasicDefinitions]

T

tff_transition_dec [in OAut.Complement]
tilde_w_equivalence [in OAut.Ramsey]
toProp_dec [in FinTypes.Automata]
transforms_final_extensional [in OAut.Complement]
transforms_extensional [in OAut.Complement]
transition_dec_public [in OAut.NFAs]
True_dec [in FinTypes.External]
True_eq_dec [in FinTypes.BasicDefinitions]

U

unfold_proper [in OAut.Seqs]
unit_eq_dec [in FinTypes.BasicDefinitions]
update_proper [in OAut.AbstractMSO]
up_classic [in OAut.MSO]
up_zip_proper [in OAut.Seqs]
up_map_proper [in OAut.Seqs]
up_equal_Equivalence [in OAut.Seqs]

V

valid_path_proper [in OAut.NFAs]
valid_run_proper [in OAut.NFAs]
vector_eq_dec [in FinTypes.FinTypes]

Abbreviation Index

A

all_not_a [in OAut.NecessityAR]

B

buechi_equiv [in OAut.Complement]

E

EqClassPair [in OAut.Complement]

F

F [in OAut.NecessityAR]
F [in OAut.Ramsey]
free_are_sings [in OAut.AbstractMSO]

I

infinite [in OAut.Seqs]
infinite [in OAut.Seqs]
in_lang [in FinTypes.Automata]
in_lang [in FinTypes.Automata]

L

len [in OAut.NFAs]
list_are_sings [in OAut.AbstractMSO]
loop'b [in OAut.Seqs]

N

no_a [in OAut.NecessityAR]

O

omega_sat [in OAut.MSO]

P

PathTriple [in OAut.NFAs]

R

ramsey_state [in OAut.NecessityAR]
run [in OAut.NFAs]

S

SeqLang [in OAut.Seqs]
some_a [in OAut.NecessityAR]
some_a [in OAut.NecessityAR]
split_pos [in OAut.Seqs]
state [in OAut.NecessityAR]
state [in OAut.NecessityAR]
str [in OAut.NFAs]
StringLang [in OAut.Seqs]

T

transformsBehavior [in OAut.Complement]

U

update [in OAut.NecessityAR]
up_sat [in OAut.MSO]

V

valid_triple [in OAut.NFAs]
vP [in OAut.NecessityAR]
vX [in OAut.NecessityAR]

Definition Index

A

accept [in FinTypes.Automata]
accepting [in OAut.Buechi]
activeW [in OAut.Buechi]
ADD [in OAut.Ramsey]
addEqClass [in OAut.Complement]
AdditiveRamsey [in OAut.Ramsey]
ADD_formula [in OAut.NecessityAR]
ADD_formula' [in OAut.NecessityAR]
ADD' [in OAut.Ramsey]
admissible [in FinTypes.FinTypes]
admits_idempotent_ramseyan_factorization [in OAut.Ramsey]
admits_ramseyan_factorization [in OAut.Ramsey]
all_fin_nfa [in OAut.NecessityAR]
all_not_nfa [in OAut.NecessityAR]
applyVect [in FinTypes.FinTypes]
APreImage [in OAut.ASStructures]
ARC [in OAut.MSO]
aseq_equal [in OAut.ASStructures]
associative [in OAut.Ramsey]
at_least_one_nfa [in OAut.NecessityAR]

B

begin_in [in OAut.Seqs]
bigAnd [in OAut.AbstractMSO]
bigEx2 [in OAut.AbstractMSO]
bigOr [in OAut.AbstractMSO]
bigpi [in OAut.ASStructures]
bigUpdate2 [in OAut.AbstractMSO]
bigUpdate2Spec [in OAut.AbstractMSO]
bigzip [in OAut.ASStructures]
bigzip' [in OAut.ASStructures]
big_sintersection [in OAut.RegularLanguages]
big_intersection [in OAut.Buechi]
big_union [in OAut.Buechi]
bijective [in FinTypes.BasicDefinitions]
bot [in OAut.AbstractMSO]
buechi_language [in OAut.Buechi]
buechi_equiv_class_aut [in OAut.Complement]
buechi_eq_class [in OAut.Complement]

C

card [in FinTypes.External]
Cardinality [in FinTypes.FinTypes]
Card_X_eq [in FinTypes.FinTypes]
classifier [in OAut.Complement]
coloring_additive [in OAut.Ramsey]
ComplClosed [in OAut.NecessityAR]
complement [in FinTypes.Automata]
complement [in OAut.Complement]
complement_auts [in OAut.Complement]
concat [in FinTypes.Automata]
concat_delta_Q [in FinTypes.Automata]
concat_delta [in FinTypes.Automata]
concat_acc_decPred [in FinTypes.Automata]
concat_acc_pred [in FinTypes.Automata]
concat_inf [in OAut.Seqs]
concat_inf_indices [in OAut.Seqs]
concat_strings [in OAut.Seqs]
cons [in FinTypes.Automata]
const [in OAut.ASStructures]
ConstLengthString [in OAut.Seqs]
constSeq [in OAut.MSO]
constStr [in OAut.MSO]
convRemInv [in OAut.FinType]
count [in FinTypes.BasicDefinitions]
Cover [in OAut.MSO]
create_Le_K [in OAut.FinType]
critical_index [in OAut.ASStructures]
critical_index_unfold [in OAut.ASStructures]
cut [in OAut.Seqs]
cut_loop [in OAut.NFAs]
cut_string [in OAut.Seqs]

D

dec [in FinTypes.External]
decision [in FinTypes.External]
deltaCons [in FinTypes.Automata]
delta_Q_star [in FinTypes.Automata]
delta_star [in FinTypes.Automata]
diff [in FinTypes.Automata]
disjoint [in FinTypes.External]
drop [in OAut.Seqs]
drop_string_end [in OAut.Seqs]
drop_string_begin [in OAut.Seqs]

E

econcat [in OAut.Complement]
elem [in FinTypes.FinTypes]
elemToFinType [in OAut.ASStructures]
empty [in FinTypes.Automata]
empty_aut [in OAut.Buechi]
empty_language [in OAut.BasicDefs]
Epsilon_autom [in FinTypes.Automata]
EqBool [in FinTypes.BasicDefinitions]
eqClass [in OAut.Complement]
EqClass [in OAut.Complement]
EqEmpty_set [in FinTypes.BasicDefinitions]
EqFalse [in FinTypes.BasicDefinitions]
EqLe_K [in OAut.FinType]
EqList [in FinTypes.BasicDefinitions]
EqNat [in FinTypes.BasicDefinitions]
EqOption [in FinTypes.BasicDefinitions]
EqProd [in FinTypes.BasicDefinitions]
EqSigT [in FinTypes.BasicDefinitions]
EqSubType [in FinTypes.BasicDefinitions]
EqSum [in FinTypes.BasicDefinitions]
EqTrue [in FinTypes.BasicDefinitions]
equi [in FinTypes.External]
equiv_class [in OAut.FinType]
equiv_merge_subseq [in OAut.Ramsey]
EqUnit [in FinTypes.BasicDefinitions]
EqVect [in FinTypes.FinTypes]
EString [in OAut.Complement]
exactW [in FinTypes.Automata]
exact_up_nfa [in OAut.Buechi]
Example1 [in FinTypes.FinTypes]
Example1 [in FinTypes.FinTypes]
Example2 [in FinTypes.FinTypes]
Example2 [in FinTypes.FinTypes]
expl [in FinTypes.FinTypes]
extensionalPower [in FinTypes.FinTypes]
extract [in OAut.Seqs]

F

FAll [in OAut.AbstractMSO]
FCIter [in FinTypes.FinTypes]
FCStep [in FinTypes.FinTypes]
filter [in FinTypes.External]
final [in OAut.Buechi]
final_loop_exists [in OAut.Buechi]
finBigAnd [in OAut.AbstractMSO]
finBigEx2 [in OAut.AbstractMSO]
finBigOr [in OAut.AbstractMSO]
finBigUpdate2 [in OAut.AbstractMSO]
finite [in OAut.NecessityAR]
finiteIndex [in OAut.Ramsey]
FInter [in OAut.AbstractMSO]
finType_fromList [in FinTypes.FinTypes]
finType_sub [in FinTypes.FinTypes]
finType_sigT [in FinTypes.FinTypes]
finType_vector [in FinTypes.FinTypes]
finType_sum [in FinTypes.FinTypes]
finType_BoolUnit [in FinTypes.FinTypes]
finType_Option [in FinTypes.FinTypes]
finType_Prod [in FinTypes.FinTypes]
finType_False [in FinTypes.FinTypes]
finType_True [in FinTypes.FinTypes]
finType_Empty_set [in FinTypes.FinTypes]
finType_bool [in FinTypes.FinTypes]
finType_unit [in FinTypes.FinTypes]
finType_cc [in FinTypes.FinTypes]
finType_Le_K [in OAut.FinType]
fin_nfa [in OAut.NecessityAR]
fin_iter [in OAut.Seqs]
first [in OAut.BasicDefs]
fix_first_zero [in OAut.Seqs]
formulaNFA [in OAut.MSO]
formula_language [in OAut.MSO]
fp [in FinTypes.FinTypes]
free_sings [in OAut.AbstractMSO]
free_sings' [in OAut.AbstractMSO]
free_svars [in OAut.AbstractMSO]
free_fvars [in OAut.AbstractMSO]
free_vars [in OAut.AbstractMSO]
fromFinTypeFromList [in OAut.FinType]
from_ind_nfa [in OAut.RegularLanguages]
FVar [in OAut.AbstractMSO]

G

getAt [in FinTypes.FinTypes]
getImage [in FinTypes.FinTypes]
getPosition [in FinTypes.FinTypes]
getX [in OAut.MSO]
getY [in OAut.MSO]
get_equiv_class [in OAut.FinType]
get_equiv_class_rep [in OAut.FinType]

H

has_monochromatic_subsequence [in OAut.Ramsey]
holdsIn [in OAut.Seqs]

I

idempotent [in OAut.Ramsey]
id_Le_K [in OAut.FinType]
image [in FinTypes.FinTypes]
Image [in OAut.Seqs]
images [in FinTypes.FinTypes]
image_aut [in OAut.Buechi]
image_transition [in OAut.Buechi]
inclp [in FinTypes.External]
incl_nfa [in OAut.MSO]
incl_transition [in OAut.MSO]
incl_state [in OAut.MSO]
index [in FinTypes.FinTypes]
infiniteP [in OAut.Seqs]
InfinitePigeonholePrinciple [in OAut.Ramsey]
infinite_filter [in OAut.Seqs]
initial [in OAut.Buechi]
injective [in FinTypes.BasicDefinitions]
intersect [in FinTypes.Automata]
intersect [in OAut.Buechi]
intersection_transition [in OAut.Buechi]
intersection_final [in OAut.Buechi]
intersection_initial [in OAut.Buechi]
intersection_state [in OAut.Buechi]
interToSeq [in OAut.MSO]
in_vP [in OAut.NecessityAR]
in_equiv_class [in OAut.FinType]
irun [in OAut.Buechi]
IsSucc [in OAut.AbstractMSO]
IsSuccMem [in OAut.AbstractMSO]
is_ramseyan_factorization [in OAut.Ramsey]
ItoM0 [in OAut.AbstractMSO]
ItoM1 [in OAut.AbstractMSO]
ItoM2 [in OAut.AbstractMSO]
I2chain [in OAut.MSO]

J

join [in OAut.FinType]
joinASeq [in OAut.MSO]

K

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

L

LAmap [in OAut.ASStructures]
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 FinTypes.Automata]
lang_incl [in FinTypes.Automata]
lang_prepend [in OAut.Seqs]
lang_o_iter [in OAut.Seqs]
LAproj_list [in OAut.MSO]
least_fp_containing [in FinTypes.FinTypes]
Leq [in OAut.AbstractMSO]
less_nfa [in OAut.MSO]
less_transition [in OAut.MSO]
less_state [in OAut.MSO]
Le_K [in OAut.FinType]
le_k [in OAut.FinType]
list_proj_aut [in OAut.MSO]
logic_dec [in OAut.BasicDefs]
L_dind [in OAut.RegularLanguages]
L_ind [in OAut.RegularLanguages]
L_A [in OAut.ASStructures]

M

Markov [in OAut.Ramsey]
max_of_nat_string [in OAut.Ramsey]
mC [in FinTypes.FinTypes]
memX [in OAut.MSO]
minsat [in OAut.AbstractMSO]
mmC [in FinTypes.FinTypes]
MNotEmpty [in OAut.AbstractMSO]
msatisfies [in OAut.AbstractMSO]
MSingleton [in OAut.AbstractMSO]
MSO_Classical [in OAut.NecessityAR]
mso_impl [in OAut.AbstractMSO]
mso_equiv [in OAut.AbstractMSO]
mul [in OAut.Ramsey]
MyhillNerode [in OAut.Complement]

N

narrowASeq [in OAut.MSO]
narrowVector [in OAut.FinType]
NatCover [in OAut.MSO]
NatPartition [in OAut.MSO]
NatUnique [in OAut.MSO]
nat_pair_le [in OAut.Seqs]
nat_to_pair [in OAut.Ramsey]
neg_F [in FinTypes.Automata]
next_position_exists [in OAut.Seqs]
next_position [in OAut.Seqs]
nfa_omega_iter [in OAut.Buechi]
nfa_omega_iter' [in OAut.Buechi]
normalize [in OAut.RegularLanguages]
normalize_final [in OAut.RegularLanguages]
normalize_inital [in OAut.RegularLanguages]
norm_transition [in OAut.RegularLanguages]
norm_final_state [in OAut.RegularLanguages]
norm_initial_state [in OAut.RegularLanguages]
norm_state [in OAut.RegularLanguages]
nums_leq_K [in OAut.FinType]
n_accept [in FinTypes.Automata]

O

oiter_transition [in OAut.Buechi]
OmegaSequenceStructure [in OAut.ASStructures]
OmegaStructure [in OAut.ASStructures]
omega_iteration [in OAut.Seqs]
onestate [in FinTypes.Automata]
Or [in OAut.AbstractMSO]
os_accepting_run [in OAut.RegularLanguages]
os_nfa [in OAut.RegularLanguages]
os_transition [in OAut.RegularLanguages]
os_final [in OAut.RegularLanguages]
os_initial [in OAut.RegularLanguages]
os_state [in OAut.RegularLanguages]

P

Pairs [in OAut.Ramsey]
pair_to_nat [in OAut.Ramsey]
Partition [in OAut.MSO]
path [in OAut.NFAs]
pickx [in FinTypes.FinTypes]
power [in FinTypes.External]
predCons [in FinTypes.Automata]
PreImage [in OAut.Seqs]
preimage_aut [in OAut.Buechi]
prepend [in OAut.Seqs]
prepend_nfa [in OAut.Buechi]
prepend_nfa' [in OAut.Buechi]
prepend_state_initial [in OAut.Buechi]
prepend_state_final [in OAut.Buechi]
prepend_transition [in OAut.Buechi]
prepend_state [in OAut.Buechi]
prepend_string [in OAut.Seqs]
prepend_prefix [in OAut.Seqs]
prod [in FinTypes.Automata]
prodLists [in FinTypes.BasicDefinitions]
prod_F [in FinTypes.Automata]
prod_pred [in FinTypes.Automata]
prod_delta [in FinTypes.Automata]
pure [in FinTypes.BasicDefinitions]
pure_W_final [in OAut.Complement]

R

RamseyFac [in OAut.Ramsey]
ramsey_nfa [in OAut.NecessityAR]
ramsey_idem_aut [in OAut.NecessityAR]
ramsey_idem_aut'_run [in OAut.NecessityAR]
ramsey_idem_aut' [in OAut.NecessityAR]
ramsey_transition [in OAut.NecessityAR]
reach [in FinTypes.Automata]
reachable [in OAut.NFAs]
reachable_with [in FinTypes.Automata]
refines [in OAut.Complement]
rem [in FinTypes.External]
rem_loops [in OAut.NFAs]
rem_loops' [in OAut.NFAs]
rep [in FinTypes.External]
rest [in OAut.FinType]
right_congruent [in OAut.Complement]
Run [in OAut.NFAs]
run_for_transforms [in OAut.Complement]
r' [in OAut.Complement]
R' [in OAut.Complement]

S

saccepting [in OAut.RegularLanguages]
SAll [in OAut.AbstractMSO]
sat [in OAut.AbstractMSO]
satisfies [in OAut.AbstractMSO]
sautomaton_normalized [in OAut.RegularLanguages]
scomplement [in OAut.RegularLanguages]
sdiff [in OAut.RegularLanguages]
seaccepting [in OAut.Complement]
selanguage [in OAut.Complement]
selectX [in OAut.MSO]
separate [in OAut.FinType]
Seq [in OAut.Seqs]
SeqLang_Extensional [in OAut.Seqs]
seqToInter [in OAut.MSO]
seqToList [in OAut.RegularLanguages]
seqToSet [in OAut.MSO]
seq_to_sets [in OAut.NecessityAR]
seq_zip [in OAut.Seqs]
seq_map [in OAut.Seqs]
seq_equal [in OAut.Seqs]
setEquiv [in OAut.AbstractMSO]
setless [in OAut.AbstractMSO]
setToSeq [in OAut.MSO]
sfinal [in OAut.RegularLanguages]
sgBoolAnd [in OAut.Ramsey]
sinitial [in OAut.RegularLanguages]
SInter [in OAut.AbstractMSO]
SInterExtensional [in OAut.AbstractMSO]
sintersect [in OAut.RegularLanguages]
slanguage [in OAut.RegularLanguages]
special_states [in OAut.RegularLanguages]
split_second [in OAut.Seqs]
split_first [in OAut.Seqs]
step_consistent [in FinTypes.FinTypes]
step_reach [in FinTypes.Automata]
StringLang_Extensional [in OAut.Seqs]
strings_equal [in OAut.Seqs]
stringToList [in OAut.RegularLanguages]
string_zip [in OAut.Seqs]
string_map [in OAut.Seqs]
subset [in OAut.AbstractMSO]
subtype [in FinTypes.BasicDefinitions]
success2 [in FinTypes.FinTypes]
success3 [in FinTypes.FinTypes]
sunion [in OAut.RegularLanguages]
surjective [in FinTypes.BasicDefinitions]
svalid [in OAut.RegularLanguages]
SVar [in OAut.AbstractMSO]
swap [in OAut.Seqs]
swap_sum [in OAut.Buechi]
s_s'_pair_aut [in OAut.Complement]
s_monotone [in OAut.Seqs]

T

tff_aut [in OAut.Complement]
tff_transition [in OAut.Complement]
tff_state [in OAut.Complement]
tf_aut [in OAut.Complement]
tilde_w_equiv_mso [in OAut.NecessityAR]
tilde_w_equiv [in OAut.Ramsey]
toBool [in FinTypes.BasicDefinitions]
toDFA [in FinTypes.Automata]
toDFA_delta [in FinTypes.Automata]
toDFA_F [in FinTypes.Automata]
toeqType [in FinTypes.BasicDefinitions]
tofinType [in FinTypes.FinTypes]
toFinTypeFromList [in OAut.FinType]
toL_A [in OAut.ASStructures]
toMinMSO [in OAut.AbstractMSO]
toNFA [in FinTypes.Automata]
toOptionList [in FinTypes.BasicDefinitions]
top [in OAut.AbstractMSO]
toProp [in FinTypes.Automata]
toSigTList [in FinTypes.FinTypes]
toSubList [in FinTypes.FinTypes]
toSumList1 [in FinTypes.BasicDefinitions]
toSumList2 [in FinTypes.BasicDefinitions]
toV1 [in OAut.AbstractMSO]
toV2 [in OAut.AbstractMSO]
to_ind_nfa [in OAut.RegularLanguages]
to_bounded [in OAut.Seqs]
to_seq [in OAut.Seqs]
transforms [in OAut.Complement]
transforms_final [in OAut.Complement]
transition_all [in OAut.NecessityAR]
transition_at_least_one [in OAut.NecessityAR]

U

U [in FinTypes.Automata]
undup [in FinTypes.External]
unfold [in OAut.Seqs]
union [in OAut.Buechi]
union_final [in OAut.Buechi]
union_initial [in OAut.Buechi]
union_transition [in OAut.Buechi]
union_state [in OAut.Buechi]
Unique [in OAut.MSO]
universal_language [in OAut.BasicDefs]
univ_aut [in OAut.NFAs]
UPDet [in OAut.NecessityAR]
upgrade_bound [in OAut.FinType]
UPSequenceStructure [in OAut.ASStructures]
UPStructure [in OAut.ASStructures]
up_zip [in OAut.Seqs]
up_zip'' [in OAut.Seqs]
up_zip' [in OAut.Seqs]
up_map [in OAut.Seqs]
up_equal [in OAut.Seqs]

V

valid_path [in OAut.NFAs]
valid_run [in OAut.NFAs]
vars_for_elems [in OAut.NecessityAR]
vars_for_list [in OAut.NecessityAR]
vector [in FinTypes.FinTypes]
vectorise [in FinTypes.FinTypes]
visits_final [in OAut.Complement]
VW_part_of_complement [in OAut.Complement]
VW_aut [in OAut.Complement]

W

word [in FinTypes.Automata]
W_final [in OAut.Complement]

X

XM_WordProblem [in OAut.NecessityAR]

Z

ZeroEl [in OAut.AbstractMSO]
zipFinTypes [in OAut.ASStructures]

Record Index

A

AdmissibleSequenceStructure [in OAut.ASStructures]

D

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

E

eqType [in FinTypes.External]

F

FiniteSemigroup [in OAut.Ramsey]
finType [in FinTypes.FinTypes]
finTypeC [in FinTypes.FinTypes]

N

NatSetClass [in OAut.AbstractMSO]
NFA [in OAut.NFAs]
nfa [in FinTypes.Automata]

S

SequenceStructure [in OAut.ASStructures]
String [in OAut.Seqs]

U

UPSeq [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

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

(92 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

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

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

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

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

(14 entries)