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

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

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

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

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

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

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

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

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

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

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

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

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

(16 entries)

---

Global Index

A

AbstractAutomata [record, in Buechi.MinimalS1S]
AbstractSequence [record, in Buechi.Sequences]
AC [definition, in Buechi.NecessityRF]
accepted_strings_transforms [lemma, in Buechi.Buechi]
accepted_strings_transforms' [lemma, in Buechi.Buechi]
accepting [definition, in Buechi.Buechi]
accepting_dec_public [instance, in Buechi.NFAs]
accepting_state_dec [projection, in Buechi.NFAs]
accepting_state [projection, in Buechi.NFAs]
accepting_quasi_run_iff_accepts [lemma, in Buechi.Buechi]
accepting_implies_quasirun [lemma, in Buechi.Buechi]
accepting_quasi_run [definition, in Buechi.Buechi]
accepting_for_proper [instance, in Buechi.Buechi]
accepting_proper [instance, in Buechi.Buechi]
accepting_extensional [lemma, in Buechi.Buechi]
accepting_for [definition, in Buechi.Buechi]
accepts [definition, in Buechi.Buechi]
accepts_proper [instance, in Buechi.Buechi]
accept_step [constructor, in Buechi.RegularLanguages]
accept_empty [constructor, in Buechi.RegularLanguages]
ACIffRF [section, in Buechi.NecessityRF]
ACIffRF.RamseyNFA [section, in Buechi.NecessityRF]
AC_equiv_RF [lemma, in Buechi.NecessityRF]
AC_implies_AX [lemma, in Buechi.NecessityRF]
add [projection, in Buechi.FiniteSemigroups]
addGamma [definition, in Buechi.Complement]
addGamma_is_associative [lemma, in Buechi.Complement]
additive [definition, in Buechi.AdditiveRamsey]
AdditiveRamsey [section, in Buechi.AdditiveRamsey]
AdditiveRamsey [library]
additive_to_substr' [lemma, in Buechi.AdditiveRamsey]
admissible [definition, in FinTypes.FinTypes]
admits_ramseyan_fac_iff_idem_ramseyan_fac [lemma, in Buechi.RamseyanFactorizations]
admits_ramseyan_factorization_proper [instance, in Buechi.RamseyanFactorizations]
admits_idempotent_ramseyan_factorization [definition, in Buechi.RamseyanFactorizations]
admits_ramseyan_factorization [definition, in Buechi.RamseyanFactorizations]
allSub [lemma, in FinTypes.FinTypes]
all_sings [definition, in Buechi.FullS1S]
all_aut_correct [lemma, in Buechi.NecessityRF]
all_aut [definition, in Buechi.NecessityRF]
all1_correct [lemma, in Buechi.FullS1S]
all2_correct [lemma, in Buechi.FullS1S]
And [constructor, in Buechi.FullS1S]
and_dec [instance, in FinTypes.External]
and_correct [lemma, in Buechi.FullS1S]
annotate [definition, in Buechi.Sequences]
annotate_correct [lemma, in Buechi.Sequences]
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]
Assoc [projection, in Buechi.FiniteSemigroups]
associative [definition, in Buechi.FiniteSemigroups]
AU [definition, in Buechi.NecessityRF]
Aut [projection, in Buechi.MinimalS1S]
autU_accepted_by_aut1 [lemma, in Buechi.Buechi]
aut_lang_sat_xm [lemma, in Buechi.MinimalS1S]
aut_forall_sums_different [lemma, in Buechi.NecessityRF]
aut_all_sums_different [definition, in Buechi.NecessityRF]
aut_inf_merging_correct [lemma, in Buechi.NecessityRF]
aut_exists_inf_merging_correct [lemma, in Buechi.NecessityRF]
aut_inf_merging [definition, in Buechi.NecessityRF]
aut_accepts_nfa_omega_iter [lemma, in Buechi.Buechi]
aut_accepts_image [lemma, in Buechi.Buechi]
aut1_incl_autU [lemma, in Buechi.Buechi]
AU_equiv_AC [lemma, in Buechi.NecessityRF]
AX [definition, in Buechi.NecessityRF]
AXImpliesRP [section, in Buechi.NecessityRF]
AXImpliesRP.AutAll [section, in Buechi.NecessityRF]
AXImpliesRP.AutAll.P [variable, in Buechi.NecessityRF]
AXImpliesRP.ax [variable, in Buechi.NecessityRF]
AXImpliesRP.ExAut [section, in Buechi.NecessityRF]
AXImpliesRP.ExAut.P [variable, in Buechi.NecessityRF]
AXImpliesRP.SatXM_RP.MergesAut [section, in Buechi.NecessityRF]
AXImpliesRP.SatXM_RP [section, in Buechi.NecessityRF]
AXImpliesRP.SuffixSumsAut [section, in Buechi.NecessityRF]
AXImpliesRP.SumAut [section, in Buechi.NecessityRF]
AX_implies_RP [lemma, in Buechi.NecessityRF]

B

B [abbreviation, in Buechi.FullS1S]
BaseSeqOperations [section, in Buechi.Sequences]
_ +++ _ [notation, in Buechi.Sequences]
BasicDefinitions [library]
begin_pos_smonotone [lemma, in Buechi.AdditiveRamsey]
begin_pos [definition, in Buechi.AdditiveRamsey]
between_accepting_state_transforms_not_accepting [lemma, in Buechi.Buechi]
between_accepting_state_transforms_not_accepting' [lemma, in Buechi.Buechi]
between_accepting_state_intersect_is_accepting_state_aut_1 [lemma, in Buechi.Buechi]
bigAnd [definition, in Buechi.FullS1S]
bigAndCorrect [lemma, in Buechi.FullS1S]
bigEx2 [definition, in Buechi.FullS1S]
bigEx2_correct [lemma, in Buechi.FullS1S]
bigOr [definition, in Buechi.FullS1S]
bigOrCorrect [lemma, in Buechi.FullS1S]
bigpi [definition, in Buechi.Sequences]
bigpi_bigzip_inv [lemma, in Buechi.Sequences]
bigpi_proper [instance, in Buechi.Sequences]
bigpi_correct [lemma, in Buechi.Sequences]
bigUpdate2 [definition, in Buechi.FullS1S]
bigUpdate2_update [lemma, in Buechi.FullS1S]
bigUpdate2_unchanged [lemma, in Buechi.FullS1S]
bigUpdate2_correct [definition, in Buechi.FullS1S]
bigzip [definition, in Buechi.Sequences]
bigzip_correct [lemma, in Buechi.Sequences]
bigzip_correct' [lemma, in Buechi.Sequences]
bigzip' [definition, in Buechi.Sequences]
big_or_false [lemma, in Buechi.RamseyanFactorizations]
big_or_true [lemma, in Buechi.RamseyanFactorizations]
big_union_correct [lemma, in Buechi.Buechi]
big_union [definition, in Buechi.Buechi]
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 Buechi.FullS1S]
bot_correct [lemma, in Buechi.FullS1S]
bounded_strict_forall [instance, in Buechi.Utils]
bounded_exist [instance, in Buechi.Utils]
bounded_forall [instance, in Buechi.Utils]
bounded_pred [lemma, in Buechi.Utils]
Buechi [section, in Buechi.Buechi]
Buechi [library]
BuechiAbstractAutomaton [instance, in Buechi.MinimalS1S]
Buechi.BuechiAutomaton [section, in Buechi.Buechi]
Buechi.BuechiAutomaton.aut [variable, in Buechi.Buechi]
Buechi.ImageNFA [section, in Buechi.Buechi]
Buechi.ImageNFA.aut [variable, in Buechi.Buechi]
Buechi.ImageNFA.f [variable, in Buechi.Buechi]
Buechi.Intersection [section, in Buechi.Buechi]
Buechi.Intersection.aut_2 [variable, in Buechi.Buechi]
Buechi.Intersection.aut_1 [variable, in Buechi.Buechi]
Buechi.Intersection.IRun [section, in Buechi.Buechi]
Buechi.Intersection.IRun.F1 [variable, in Buechi.Buechi]
Buechi.Intersection.IRun.F2 [variable, in Buechi.Buechi]
Buechi.Intersection.IRun.rho_2 [variable, in Buechi.Buechi]
Buechi.Intersection.IRun.rho_1 [variable, in Buechi.Buechi]
Buechi.Intersection.IRun.sigma [variable, in Buechi.Buechi]
Buechi.Match [section, in Buechi.Buechi]
Buechi.Match.aut [variable, in Buechi.Buechi]
Buechi.NFAOmegaIteration [section, in Buechi.Buechi]
Buechi.NFAOmegaIteration.aut [variable, in Buechi.Buechi]
Buechi.PreImageNFA [section, in Buechi.Buechi]
Buechi.PreImageNFA.aut [variable, in Buechi.Buechi]
Buechi.PreImageNFA.f [variable, in Buechi.Buechi]
Buechi.PrependNFA [section, in Buechi.Buechi]
Buechi.PrependNFA.aut_2 [variable, in Buechi.Buechi]
Buechi.PrependNFA.aut_1 [variable, in Buechi.Buechi]
Buechi.QuasiRun [section, in Buechi.Buechi]
Buechi.QuasiRun.aut [variable, in Buechi.Buechi]
Buechi.QuasiRun.QuasiRunImpliesAccepting [section, in Buechi.Buechi]
Buechi.QuasiRun.QuasiRunImpliesAccepting.Acc [variable, in Buechi.Buechi]
Buechi.QuasiRun.QuasiRunImpliesAccepting.rho [variable, in Buechi.Buechi]
Buechi.QuasiRun.QuasiRunImpliesAccepting.tau [variable, in Buechi.Buechi]
Buechi.SimpleAutomata [section, in Buechi.Buechi]
Buechi.Union [section, in Buechi.Buechi]
Buechi.Union.Def [section, in Buechi.Buechi]
Buechi.Union.Def.aut_2 [variable, in Buechi.Buechi]
Buechi.Union.Def.aut_1 [variable, in Buechi.Buechi]
L_B [notation, in Buechi.Buechi]

C

card [definition, in FinTypes.External]
card [definition, in Buechi.FinSets]
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' [definition, in Buechi.FinSets]
cc_j_k [definition, in Buechi.RamseyanPigeonholePrinciple]
cc_nat_first_geq_exists_extensional [lemma, in Buechi.Utils]
cc_nat_first_geq_exists_extensional' [lemma, in Buechi.Utils]
cc_nat_first_geq_exists_eq [lemma, in Buechi.Utils]
cc_nat_first_geq_exists_all [lemma, in Buechi.Utils]
cc_nat_first_geq_exists_correct [lemma, in Buechi.Utils]
cc_nat_first_geq_exists_increasing [lemma, in Buechi.Utils]
cc_nat_first_geq_exists [definition, in Buechi.Utils]
cc_nat_first_geq_all [lemma, in Buechi.Utils]
cc_nat_first_geq_bounds [lemma, in Buechi.Utils]
cc_nat_first_geq_correct [lemma, in Buechi.Utils]
cc_nat_first_geq [definition, in Buechi.Utils]
cc_nat_first_extensional [lemma, in Buechi.Utils]
cc_nat [lemma, in Buechi.Utils]
cc_nat_first [lemma, in Buechi.Utils]
choose_sym_correct [lemma, in Buechi.Buechi]
choose_sym [definition, in Buechi.Buechi]
class [projection, in FinTypes.FinTypes]
ClassicalReasoning [section, in Buechi.FullS1S]
clear_X [definition, in Buechi.MinimalS1S]
closed_prefix_map [lemma, in Buechi.Sequences]
closed_substr_prepend [lemma, in Buechi.Sequences]
closed_prefix_eq [lemma, in Buechi.Sequences]
closed_substr_proper [instance, in Buechi.Sequences]
closed_prefix_proper [instance, in Buechi.Sequences]
closed_substr_nstr_drop [lemma, in Buechi.Sequences]
closed_substr_singleton [lemma, in Buechi.Sequences]
closed_substr_shift [lemma, in Buechi.Sequences]
closed_substr_step_last [lemma, in Buechi.Sequences]
closed_substr_step [lemma, in Buechi.Sequences]
closed_substr_begin [lemma, in Buechi.Sequences]
closed_substr_nth' [lemma, in Buechi.Sequences]
closed_substr_nth [lemma, in Buechi.Sequences]
closed_prefix_plus [lemma, in Buechi.Sequences]
closed_prefix_step [lemma, in Buechi.Sequences]
closed_prefix_nth [lemma, in Buechi.Sequences]
closed_substr_delta [lemma, in Buechi.Sequences]
closed_prefix_delta [lemma, in Buechi.Sequences]
closed_substr [definition, in Buechi.Sequences]
closed_prefix [definition, in Buechi.Sequences]
closed_take_delta [lemma, in Buechi.Strings]
closed_take [definition, in Buechi.Strings]
Closure [lemma, in FinTypes.FinTypes]
Closure_FCIter [lemma, in FinTypes.FinTypes]
color_transition [definition, in Buechi.RegularLanguages]
combine_sum [lemma, in Buechi.RamseyanFactorizations]
combine_transforms_accepting_right [lemma, in Buechi.NFAs]
combine_transforms_accepting_left [lemma, in Buechi.NFAs]
combine_transforms [lemma, in Buechi.NFAs]
compatibility [lemma, in Buechi.Complement]
complement [definition, in Buechi.Complement]
Complement [section, in Buechi.Complement]
Complement [library]
complement_exhaustive_up [lemma, in Buechi.Complement]
complement_exhaustive [lemma, in Buechi.Complement]
complement_kind_exhaustive [lemma, in Buechi.Complement]
complement_disjoint [lemma, in Buechi.Complement]
complement_aut_correct [lemma, in Buechi.MinimalS1S]
complement_aut_exhaustive [projection, in Buechi.MinimalS1S]
complement_aut_disjoint [projection, in Buechi.MinimalS1S]
complement_aut [projection, in Buechi.MinimalS1S]
Complement.aut [variable, in Buechi.Complement]
{[ _ ]} [notation, in Buechi.Complement]
complete_induction [lemma, in Buechi.Utils]
compute_run [definition, in Buechi.Buechi]
concat_map_length [lemma, in FinTypes.FinTypes]
consAppend [lemma, in FinTypes.BasicDefinitions]
const [projection, in Buechi.Sequences]
const_nth [lemma, in Buechi.Sequences]
const_correct [projection, in Buechi.Sequences]
cons_equi_proper [instance, in FinTypes.External]
cons_incl_proper [instance, in FinTypes.External]
cons_incll [lemma, in FinTypes.BasicDefinitions]
cons_admits_ramseyan_fac [lemma, in Buechi.RamseyanFactorizations]
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]
cut [definition, in Buechi.Sequences]
cut_map [lemma, in Buechi.Sequences]
cut_flatten_inv [lemma, in Buechi.Sequences]
cut_delta [lemma, in Buechi.Sequences]
cut_proper [instance, in Buechi.Sequences]
cut_correct [lemma, in Buechi.Sequences]
cut_seq [definition, in Buechi.Sequences]

D

dec [definition, in FinTypes.External]
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 Buechi.Utils]
decision_true [lemma, in Buechi.Utils]
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_min_sat_implies_dec_full_sat [lemma, in Buechi.FullS1S]
dec_singleton_sets [lemma, in Buechi.FullS1S]
dec_kind_compatible [instance, in Buechi.Complement]
dec_satisfaction_up [lemma, in Buechi.MinimalS1S]
dec_min_S1S_up_satisfaction [lemma, in Buechi.MinimalS1S]
dec_min_S1S_satisfaction [lemma, in Buechi.MinimalS1S]
dec_emptiness [projection, in Buechi.MinimalS1S]
dec_string_exists_fixed_length' [instance, in Buechi.Strings]
dec_string_exists_bounded_length [instance, in Buechi.Strings]
dec_string_exists_fixed_length [instance, in Buechi.Strings]
dec_ex_transforms_accepting [instance, in Buechi.NFAs]
dec_ex_transforms_accepting_informative [lemma, in Buechi.NFAs]
dec_ex_transforms [instance, in Buechi.NFAs]
dec_ex_transforms_informative [lemma, in Buechi.NFAs]
dec_transforms_informative_bound [lemma, in Buechi.NFAs]
dec_transforms_accepting [instance, in Buechi.NFAs]
dec_transforms [instance, in Buechi.NFAs]
dec_valid_path [instance, in Buechi.NFAs]
dec_match_bool [instance, in Buechi.Utils]
dec_destruct_list [instance, in Buechi.Utils]
dec_option [instance, in Buechi.Utils]
dec_sum [instance, in Buechi.Utils]
dec_pair [instance, in Buechi.Utils]
dec_up_in_lang [lemma, in Buechi.Buechi]
dec_mem_empty [instance, in Buechi.Buechi]
dec_is_buechi_nonempty [instance, in Buechi.Buechi]
dec_is_buechi_empty [instance, in Buechi.Buechi]
dec_buechi_empty_informative [lemma, in Buechi.Buechi]
dec_exists_match [instance, in Buechi.Buechi]
dec_is_match [lemma, in Buechi.Buechi]
delta [definition, in Buechi.Strings]
delta_length [lemma, in Buechi.Strings]
deMorgan_and' [lemma, in Buechi.Utils]
deMorgan_and [lemma, in Buechi.Utils]
deMorgan_or [lemma, in Buechi.Utils]
deMorgan_exists [lemma, in Buechi.Utils]
deMorgan_all_neg [lemma, in Buechi.Utils]
deMorgan_all [lemma, in Buechi.Utils]
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]
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]
double_flatten_cut_inv [lemma, in Buechi.Sequences]
double_negation [lemma, in Buechi.Utils]
DropTake [section, in Buechi.Strings]
drop_map [lemma, in Buechi.Sequences]
drop_proper [instance, in Buechi.Sequences]
drop_nth' [lemma, in Buechi.Sequences]
drop_nth [lemma, in Buechi.Sequences]
drop_plus [lemma, in Buechi.Sequences]
drop_tl [lemma, in Buechi.Sequences]
drop_step [lemma, in Buechi.Sequences]
dummy [projection, in Buechi.Strings]
Dummy [record, in Buechi.Strings]
dummy [constructor, in Buechi.Strings]
Dummy [inductive, in Buechi.Strings]
DummyDummy [instance, in Buechi.Strings]
DummyNat [instance, in Buechi.Strings]
DummyNatFunc [instance, in Buechi.Strings]
DummyNStr [instance, in Buechi.Strings]
Dummy_nonempty [instance, in Buechi.Strings]
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.X [variable, in FinTypes.External]
DuplicateInString [section, in Buechi.Strings]
duplicates [lemma, in Buechi.Strings]
D1 [projection, in Buechi.FullS1S]
D2 [projection, in Buechi.FullS1S]
D3 [projection, in Buechi.FullS1S]

E

elem [definition, in FinTypes.FinTypes]
ElemDummy [instance, in Buechi.Strings]
elementIn [lemma, in FinTypes.FinTypes]
elements [projection, in Buechi.FiniteSemigroups]
elemToFinType [definition, in Buechi.Sequences]
el_correct [lemma, in Buechi.FullS1S]
emptySet [definition, in Buechi.FinSets]
emptySet_correct [lemma, in Buechi.FinSets]
Empty_set_enum_ok [lemma, in FinTypes.FinTypes]
Empty_set_eq_dec [instance, in FinTypes.BasicDefinitions]
empty_language [definition, in Buechi.Utils]
empty_aut_correct [lemma, in Buechi.Buechi]
empty_aut [definition, in Buechi.Buechi]
encodes_fact_tl_revert [lemma, in Buechi.AdditiveRamsey]
encodes_fact_tl_preserves_deltas [lemma, in Buechi.AdditiveRamsey]
encodes_fact_tl [definition, in Buechi.AdditiveRamsey]
encode_seq_nth [lemma, in Buechi.NecessityRF]
encode_seq [definition, in Buechi.NecessityRF]
enum [projection, in FinTypes.FinTypes]
enum_ok_fromList [lemma, in FinTypes.FinTypes]
enum_ok [projection, in FinTypes.FinTypes]
eqtype [projection, in FinTypes.External]
eqType [record, in FinTypes.External]
EqType [constructor, in FinTypes.External]
equalize_first_delta [lemma, in Buechi.UPSequences]
equalize_first_correct [lemma, in Buechi.UPSequences]
equalize_first [definition, in Buechi.UPSequences]
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]
equiv_apart_update' [lemma, in Buechi.FullS1S]
equiv_apart_update [lemma, in Buechi.FullS1S]
equiv_apart_proper [instance, in Buechi.MinimalS1S]
equiv_apart [definition, in Buechi.MinimalS1S]
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]
eq_iff [lemma, in FinTypes.FinTypes]
eq_dec_sigT [instance, in FinTypes.BasicDefinitions]
eq_funTrans [lemma, in FinTypes.BasicDefinitions]
exact_up_nfa_correct [lemma, in Buechi.Buechi]
exact_up_nfa [definition, in Buechi.Buechi]
Example1 [definition, in FinTypes.FinTypes]
Example1 [definition, in FinTypes.FinTypes]
Example2 [definition, in FinTypes.FinTypes]
Example2 [definition, in FinTypes.FinTypes]
expl [definition, in FinTypes.FinTypes]
extensionalPower [definition, in FinTypes.FinTypes]
External [library]
extPow_length [lemma, in FinTypes.FinTypes]
ex_nfa_up [lemma, in Buechi.MinimalS1S]
ex_nfa_correct [lemma, in Buechi.MinimalS1S]
ex_nfa [definition, in Buechi.MinimalS1S]
ex_aut_correct [projection, in Buechi.MinimalS1S]
ex_aut [projection, in Buechi.MinimalS1S]
ex_transforms_accepting_cc [lemma, in Buechi.NFAs]
ex_transforms_cc [lemma, in Buechi.NFAs]
ex_aut_correct [lemma, in Buechi.NecessityRF]
ex_aut [definition, in Buechi.NecessityRF]
ex1_correct [lemma, in Buechi.FullS1S]

F

f [definition, in Buechi.RamseyanPigeonholePrinciple]
factorisation_to_bseq_correct [lemma, in Buechi.AdditiveRamsey]
factorisation_to_bseq_infinite [lemma, in Buechi.AdditiveRamsey]
factorisation_to_bseq [definition, in Buechi.AdditiveRamsey]
FactorizationsAsStrictlyMonotoneFunctions [section, in Buechi.AdditiveRamsey]
FactorizationToBooleanSequence [section, in Buechi.AdditiveRamsey]
factorize [definition, in Buechi.Sequences]
factorize_monotone [lemma, in Buechi.AdditiveRamsey]
factorize_proper [lemma, in Buechi.Sequences]
factorize_correct [lemma, in Buechi.Sequences]
FAll [definition, in Buechi.FullS1S]
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 Buechi.FullS1S]
filter [definition, in FinTypes.External]
FilterLemmas [section, in FinTypes.External]
FilterLemmas [section, in Buechi.Strings]
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.P [variable, in Buechi.Strings]
FilterLemmas.Q [variable, in Buechi.Strings]
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]
filter_partition [lemma, in Buechi.Strings]
filter_empty [lemma, in Buechi.Strings]
filter_unchanged [lemma, in Buechi.Strings]
finBigAnd [definition, in Buechi.FullS1S]
finBigAndCorrect [lemma, in Buechi.FullS1S]
finBigEx2 [definition, in Buechi.FullS1S]
finBigEx2_correct [lemma, in Buechi.FullS1S]
finBigOr [definition, in Buechi.FullS1S]
finBigOrCorrect [lemma, in Buechi.FullS1S]
finBigUpdate2 [definition, in Buechi.FullS1S]
finBigUpdate2_changed [lemma, in Buechi.FullS1S]
finBigUpdate2_unchanged [lemma, in Buechi.FullS1S]
fInduction [lemma, in FinTypes.FinTypes]
FiniteClosureIteration [section, in FinTypes.FinTypes]
FiniteClosureIteration.step [variable, in FinTypes.FinTypes]
FiniteClosureIteration.step_dec [variable, in FinTypes.FinTypes]
FiniteClosureIteration.X [variable, in FinTypes.FinTypes]
FiniteSemigroup [section, in Buechi.FiniteSemigroups]
FiniteSemigroup [record, in Buechi.FiniteSemigroups]
FiniteSemigroups [library]
FiniteSets [section, in Buechi.FinSets]
FiniteSets.X [variable, in Buechi.FinSets]
_ mem _ [notation, in Buechi.FinSets]
finSet [definition, in Buechi.FinSets]
FinSets [library]
finSet_rem_correct [lemma, in Buechi.FinSets]
finSet_rem [definition, in Buechi.FinSets]
finType [record, in FinTypes.FinTypes]
FinType [constructor, in FinTypes.FinTypes]
finTypeC [record, in FinTypes.FinTypes]
FinTypeC [constructor, in FinTypes.FinTypes]
finTypeCardAtLeast3 [record, in Buechi.FullS1S]
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]
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_sub_enum [lemma, in FinTypes.FinTypes]
finType_sub_correct [lemma, in FinTypes.FinTypes]
finType_sigT_enum [lemma, in FinTypes.FinTypes]
finType_sigT_correct [lemma, in FinTypes.FinTypes]
finType_vector_enum [lemma, in FinTypes.FinTypes]
finType_vector_correct [lemma, in FinTypes.FinTypes]
finType_BoolUnit [definition, in FinTypes.FinTypes]
finType_Prod_correct [lemma, 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]
finUnion [definition, in Buechi.FinSets]
finUnion_correct [lemma, in Buechi.FinSets]
first [definition, in Buechi.Utils]
First [section, in Buechi.Utils]
FirstGeq [section, in Buechi.Utils]
FirstGeq.f [variable, in Buechi.Utils]
FirstGeq.FirstGeq [section, in Buechi.Utils]
FirstGeq.FirstGeqExists [section, in Buechi.Utils]
FirstGeq.FirstGeqExists.L [variable, in Buechi.Utils]
FirstGeq.FirstGeq.F [variable, in Buechi.Utils]
FirstGeq.FirstGeq.L [variable, in Buechi.Utils]
FirstGeq.P [variable, in Buechi.Utils]
First.p [variable, in Buechi.Utils]
First.p_dec [variable, in Buechi.Utils]
Fixedpoints [section, in FinTypes.FinTypes]
Fixedpoints.f [variable, in FinTypes.FinTypes]
Fixedpoints.X [variable, in FinTypes.FinTypes]
flatten [definition, in Buechi.Sequences]
FlattenList [section, in Buechi.Strings]
flatten_idempotent [lemma, in Buechi.AdditiveRamsey]
flatten_concat [lemma, in Buechi.Sequences]
flatten_cut_inv [lemma, in Buechi.Sequences]
flatten_fin_iter [lemma, in Buechi.Sequences]
flatten_rotate [lemma, in Buechi.Sequences]
flatten_factorize_inv [lemma, in Buechi.Sequences]
flatten_map [lemma, in Buechi.Sequences]
flatten_prepend [lemma, in Buechi.Sequences]
flatten_correct [lemma, in Buechi.Sequences]
flatten_proper [instance, in Buechi.Sequences]
flatten_step [lemma, in Buechi.Sequences]
flatten_list [definition, in Buechi.Strings]
flatten_valid [lemma, in Buechi.NFAs]
Form [inductive, in Buechi.FullS1S]
formula_nfa_equal [lemma, in Buechi.MinimalS1S]
formula_aut_correct [lemma, in Buechi.MinimalS1S]
formula_aut [definition, in Buechi.MinimalS1S]
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]
free_sings_correct [lemma, in Buechi.FullS1S]
free_sings'_correct [lemma, in Buechi.FullS1S]
free_sings [definition, in Buechi.FullS1S]
free_sings' [definition, in Buechi.FullS1S]
free_svars [definition, in Buechi.FullS1S]
free_fvars [definition, in Buechi.FullS1S]
fresh [definition, in Buechi.FullS1S]
fresh_correct [lemma, in Buechi.FullS1S]
fromListC [instance, in FinTypes.FinTypes]
FullS1S [section, in Buechi.FullS1S]
FullS1S [library]
FullS1S.Coincidence [section, in Buechi.FullS1S]
FullS1S.Coincidence.FVar [variable, in Buechi.FullS1S]
FullS1S.Coincidence.SVar [variable, in Buechi.FullS1S]
FullS1S.ConvertInterpretations [section, in Buechi.FullS1S]
FullS1S.ConvertInterpretations.V [variable, in Buechi.FullS1S]
<\ _ |> [notation, in Buechi.FullS1S]
<| _ , _ /> [notation, in Buechi.FullS1S]
[ _ ] [notation, in Buechi.FullS1S]
<< _ , _ >> [notation, in Buechi.FullS1S]
FullS1S.ReduceFullS1S_to_MinS1S.SVar [variable, in Buechi.FullS1S]
FullS1S.ReduceFullS1S_to_MinS1S.FVar [variable, in Buechi.FullS1S]
FullS1S.ReduceFullS1S_to_MinS1S [section, in Buechi.FullS1S]
_ |= _ [notation, in Buechi.FullS1S]
_ # _ |== _ [notation, in Buechi.FullS1S]
_ [ _ := _ ] [notation, in Buechi.FullS1S]
_ elS _ [notation, in Buechi.FullS1S]
full_s1s_up_sat_if_as_sat [lemma, in Buechi.FullS1S]
full_s1s_up_sat_obtain [lemma, in Buechi.FullS1S]
full_s1s_dec_up_satisfaction [lemma, in Buechi.FullS1S]
full_s1s_dec_up_satisfies [lemma, in Buechi.FullS1S]
full_s1s_dec [lemma, in Buechi.FullS1S]
full_s1s_satisfies_xm [lemma, in Buechi.FullS1S]
full_s1s_to_min_s1s_complete [lemma, in Buechi.FullS1S]
full_s1s_to_min_s1s_correct [lemma, in Buechi.FullS1S]
function_implies_seq [lemma, in Buechi.FullS1S]
fun_encodes_factorization [definition, in Buechi.AdditiveRamsey]
FX [definition, in Buechi.FullS1S]
FXImpliesRP [section, in Buechi.NecessityRF]
FXImpliesRP.MSO_XM [variable, in Buechi.NecessityRF]
FX_implies_RP [lemma, in Buechi.NecessityRF]
FX_implies_RP_sigma [lemma, in Buechi.NecessityRF]
f_merging [lemma, in Buechi.RamseyanPigeonholePrinciple]
f_g_merge [lemma, in Buechi.RamseyanPigeonholePrinciple]
f_smonotone [lemma, in Buechi.RamseyanPigeonholePrinciple]
f_g_merging [lemma, in Buechi.RamseyanPigeonholePrinciple]

G

g [definition, in Buechi.RamseyanPigeonholePrinciple]
gamma [definition, in Buechi.Complement]
Gamma [definition, in Buechi.Complement]
gamma_is_homomorphisms [lemma, in Buechi.Complement]
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]
guess_sum_rev [lemma, in Buechi.NecessityRF]
guess_sum [lemma, in Buechi.NecessityRF]
g_smonotone [lemma, in Buechi.RamseyanPigeonholePrinciple]

H

has_some_kind [definition, in Buechi.Complement]
has_kind [definition, in Buechi.Complement]
hd [projection, in Buechi.Sequences]
hd_proper [instance, in Buechi.Sequences]
hd_correct [projection, in Buechi.Sequences]
Hedberg [lemma, in FinTypes.BasicDefinitions]
HelpApply [lemma, in FinTypes.FinTypes]
homogenous [definition, in Buechi.AdditiveRamsey]
homomorphism_cons [lemma, in Buechi.RegularLanguages]
homomorphism_singletons [lemma, in Buechi.RamseyanFactorizations]
H' [lemma, in Buechi.RamseyanPigeonholePrinciple]

I

idempotent [definition, in Buechi.FiniteSemigroups]
iff_dec [instance, in FinTypes.External]
iff_ex [lemma, in Buechi.Utils]
iff_all [lemma, in Buechi.Utils]
iff_impl_true [lemma, in Buechi.Utils]
iff_impl [lemma, in Buechi.Utils]
iff_neg [lemma, in Buechi.Utils]
Image [definition, in Buechi.Sequences]
image [definition, in FinTypes.FinTypes]
ImageProper [instance, in Buechi.Sequences]
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_match [lemma, in Buechi.Buechi]
image_aut_correct [lemma, in Buechi.Buechi]
image_accepts_aut [lemma, in Buechi.Buechi]
image_aut [definition, in Buechi.Buechi]
image_transition [definition, in Buechi.Buechi]
impl_dec [instance, in FinTypes.External]
impl_correct [lemma, in Buechi.FullS1S]
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 Buechi.MinimalS1S]
incl_nfa [definition, in Buechi.MinimalS1S]
incl_language [lemma, in Buechi.MinimalS1S]
incl_aut_correct [projection, in Buechi.MinimalS1S]
incl_aut [projection, in Buechi.MinimalS1S]
inConcatCons [lemma, in FinTypes.FinTypes]
InCount [lemma, in FinTypes.BasicDefinitions]
index [definition, in FinTypes.FinTypes]
IndexAccess [section, in Buechi.Strings]
Inf [projection, in Buechi.Sequences]
Inf [constructor, in Buechi.Sequences]
infinite [definition, in Buechi.AdditiveRamsey]
infinite_update [lemma, in Buechi.AdditiveRamsey]
infinite_bseq_to_factorisation_seg [lemma, in Buechi.AdditiveRamsey]
infinite_bseq_to_factorisation_correct [lemma, in Buechi.AdditiveRamsey]
infinite_bseq_to_factorisation [definition, in Buechi.AdditiveRamsey]
inf_often_map [lemma, in Buechi.Sequences]
inf_often_flatten [lemma, in Buechi.Sequences]
inf_often_flatten_tl [instance, in Buechi.Sequences]
inf_often_proper [instance, in Buechi.Sequences]
inf_often_prepend_instance [instance, in Buechi.Sequences]
inf_often_prepend [lemma, in Buechi.Sequences]
inf_often_cons_instance [instance, in Buechi.Sequences]
inf_often_cons [lemma, in Buechi.Sequences]
inf_often_drop [instance, in Buechi.Sequences]
inf_often_tl [instance, in Buechi.Sequences]
inf_often [record, in Buechi.Sequences]
inf_often [inductive, in Buechi.Sequences]
inf_merging_to_function [lemma, in Buechi.RamseyanPigeonholePrinciple]
inf_often_zip_offset [lemma, in Buechi.Buechi]
inImages [lemma, in FinTypes.FinTypes]
initial [definition, in Buechi.Buechi]
initial_dec_public [instance, in Buechi.NFAs]
initial_state_dec [projection, in Buechi.NFAs]
initial_state [projection, in Buechi.NFAs]
injective [definition, in FinTypes.BasicDefinitions]
injectiveApply [lemma, in FinTypes.BasicDefinitions]
injective_dupfree [lemma, in FinTypes.FinTypes]
intermediate_sum_rev [lemma, in Buechi.NecessityRF]
intermediate_sum [lemma, in Buechi.NecessityRF]
intersect [definition, in Buechi.FinSets]
intersect [definition, in Buechi.Buechi]
intersection_incl_intersect [lemma, in Buechi.Buechi]
intersection_transition [definition, in Buechi.Buechi]
intersection_accepting [definition, in Buechi.Buechi]
intersection_initial [definition, in Buechi.Buechi]
intersection_state [definition, in Buechi.Buechi]
intersect_correct [lemma, in Buechi.FinSets]
intersect_aut_correct [projection, in Buechi.MinimalS1S]
intersect_aut [projection, in Buechi.MinimalS1S]
intersect_match_second [lemma, in Buechi.Buechi]
intersect_transforms_accepting [lemma, in Buechi.Buechi]
intersect_transforms [lemma, in Buechi.Buechi]
intersect_correct [lemma, in Buechi.Buechi]
intersect_incl_aut2 [lemma, in Buechi.Buechi]
intersect_incl_aut1 [lemma, in Buechi.Buechi]
intersect_incl_aut1_acc [lemma, in Buechi.Buechi]
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_undup [lemma, in FinTypes.FinTypes]
in_complement_nfa_iff [lemma, in Buechi.Complement]
in_nstr_of_leq_delta_iff [lemma, in Buechi.Strings]
in_nstr_of_delta_iff [lemma, in Buechi.Strings]
in_flatten_list_iff [lemma, in Buechi.Strings]
in_nstr [lemma, in Buechi.Strings]
in_buechi_implies_up [lemma, in Buechi.Buechi]
IP [definition, in Buechi.RamseyanFactorizations]
IP_implies_MP [lemma, in Buechi.RamseyanFactorizations]
irun [definition, in Buechi.Buechi]
irun_accepting [lemma, in Buechi.Buechi]
irun_step_accepting [lemma, in Buechi.Buechi]
irun_step_to_true [lemma, in Buechi.Buechi]
irun_initial [lemma, in Buechi.Buechi]
irun_valid [lemma, in Buechi.Buechi]
irun_same_states [lemma, in Buechi.Buechi]
irun_Snth [lemma, in Buechi.Buechi]
irun_0th [lemma, in Buechi.Buechi]
irun_step [definition, in Buechi.Buechi]
isleft [abbreviation, in Buechi.Buechi]
isright [abbreviation, in Buechi.Buechi]
IsSucc [definition, in Buechi.FullS1S]
isSuccCorrect [lemma, in Buechi.FullS1S]
IsSuccMem [definition, in Buechi.FullS1S]
isSuccMemCorrect [lemma, in Buechi.FullS1S]
is_singleton_proper [instance, in Buechi.FullS1S]
is_singleton [definition, in Buechi.FullS1S]
is_ramseyan_factorization [definition, in Buechi.RamseyanFactorizations]
is_homomorphism [definition, in Buechi.FiniteSemigroups]
is_buechi_empty_correct [lemma, in Buechi.Buechi]
is_buechi_empty [definition, in Buechi.Buechi]
is_match [definition, in Buechi.Buechi]
ItoM0 [definition, in Buechi.FullS1S]
ItoM1 [definition, in Buechi.FullS1S]
ItoM1_agree [lemma, in Buechi.FullS1S]
ItoM1_agree' [lemma, in Buechi.FullS1S]
ItoM2 [definition, in Buechi.FullS1S]
ItoM2_agree [lemma, in Buechi.FullS1S]
ItoM2_agree' [lemma, in Buechi.FullS1S]

K

kind_compatible [definition, in Buechi.Complement]

L

lang [projection, in Buechi.MinimalS1S]
Language [definition, in Buechi.Utils]
LanguageLemmata [section, in Buechi.Utils]
LanguageLemmata.L [variable, in Buechi.Utils]
LanguageLemmata.L_2 [variable, in Buechi.Utils]
LanguageLemmata.L_1 [variable, in Buechi.Utils]
LanguageLemmata.X [variable, in Buechi.Utils]
Languages [section, in Buechi.Utils]
Languages.X [variable, in Buechi.Utils]
language_complement_proper [instance, in Buechi.Utils]
language_difference_proper [instance, in Buechi.Utils]
language_intersection_proper [instance, in Buechi.Utils]
language_union_proper [instance, in Buechi.Utils]
language_incl [instance, in Buechi.Utils]
language_eq_mem [instance, in Buechi.Utils]
language_eq_equivalence [instance, in Buechi.Utils]
language_intersection_comm [lemma, in Buechi.Utils]
language_union_comm [lemma, in Buechi.Utils]
language_eq_symmetric [lemma, in Buechi.Utils]
language_eq_iff [lemma, in Buechi.Utils]
language_universal_iff [lemma, in Buechi.Utils]
language_empty_iff [lemma, in Buechi.Utils]
language_difference [definition, in Buechi.Utils]
language_complement [definition, in Buechi.Utils]
language_intersection [definition, in Buechi.Utils]
language_union [definition, in Buechi.Utils]
language_eq [definition, in Buechi.Utils]
language_inclusion [definition, in Buechi.Utils]
Le [constructor, in Buechi.FullS1S]
least_fp_containing [definition, in FinTypes.FinTypes]
left_assoc_sum [lemma, in Buechi.RamseyanFactorizations]
left_assoc [lemma, in Buechi.RamseyanFactorizations]
lengthEq [lemma, in FinTypes.BasicDefinitions]
Leq [definition, in Buechi.FullS1S]
leq_correct [lemma, in Buechi.FullS1S]
less_nfa_correct [lemma, in Buechi.MinimalS1S]
less_nfa [definition, in Buechi.MinimalS1S]
less_language [lemma, in Buechi.MinimalS1S]
less_aut_correct [projection, in Buechi.MinimalS1S]
less_aut [projection, in Buechi.MinimalS1S]
le_correct [lemma, in Buechi.FullS1S]
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_eq [lemma, in Buechi.Utils]
loop [lemma, in FinTypes.BasicDefinitions]
loop_admits_ramseyan_fac [lemma, in Buechi.RamseyanFactorizations]

M

main_all_equiv [lemma, in Buechi.NecessityRF]
makeSet [definition, in Buechi.FinSets]
makeSet_correct [lemma, in Buechi.FinSets]
makeSet_eq [lemma, in Buechi.FinSets]
MAnd [constructor, in Buechi.MinimalS1S]
map [projection, in Buechi.Sequences]
map_nstr_prepend [lemma, in Buechi.Sequences]
map_nth [lemma, in Buechi.Sequences]
map_proper [instance, in Buechi.Sequences]
map_correct [projection, in Buechi.Sequences]
map_fst_omega [lemma, in Buechi.NecessityRF]
match_for_up [lemma, in Buechi.Buechi]
match_accepted [lemma, in Buechi.Buechi]
max_of_nat_string_correct' [lemma, in Buechi.RamseyanPigeonholePrinciple]
max_of_nat_string_correct [lemma, in Buechi.RamseyanPigeonholePrinciple]
max_of_nat_string [definition, in Buechi.RamseyanPigeonholePrinciple]
max_le [lemma, in Buechi.Utils]
max_le_right [lemma, in Buechi.Utils]
max_le_left [lemma, in Buechi.Utils]
mC [definition, in FinTypes.FinTypes]
Mem [constructor, in Buechi.FullS1S]
Membership [section, in FinTypes.External]
Membership.X [variable, in FinTypes.External]
memSet [definition, in Buechi.FullS1S]
memSetProper [instance, in Buechi.FullS1S]
mem_factorisation_to_bseq [lemma, in Buechi.AdditiveRamsey]
merge [definition, in Buechi.RamseyanPigeonholePrinciple]
merges_aut_correct [lemma, in Buechi.NecessityRF]
merges_aut [definition, in Buechi.NecessityRF]
merge_extend [lemma, in Buechi.RamseyanPigeonholePrinciple]
merge_at [definition, in Buechi.RamseyanPigeonholePrinciple]
merging_proper [instance, in Buechi.RamseyanPigeonholePrinciple]
merging_shift [lemma, in Buechi.RamseyanPigeonholePrinciple]
merging_finite_equiv_classes [lemma, in Buechi.RamseyanPigeonholePrinciple]
MEx [constructor, in Buechi.MinimalS1S]
MIncl [constructor, in Buechi.MinimalS1S]
MinForm [inductive, in Buechi.MinimalS1S]
MinimalS1S [library]
minsat_agree_as_up [lemma, in Buechi.MinimalS1S]
MinS1S [section, in Buechi.MinimalS1S]
MinS1SToBuechi [section, in Buechi.MinimalS1S]
MinS1SToBuechi.X [variable, in Buechi.MinimalS1S]
MinS1SToBuechi.Y [variable, in Buechi.MinimalS1S]
_ |= _ [notation, in Buechi.MinimalS1S]
min_sat_xm_implies_full_sat_xm [lemma, in Buechi.FullS1S]
min_sat_iff_full_sat [lemma, in Buechi.FullS1S]
min_s1S_dec_obtain [lemma, in Buechi.MinimalS1S]
min_s1S_dec_satisfaction [lemma, in Buechi.MinimalS1S]
min_s1S_dec_satisfaction_informative [lemma, in Buechi.MinimalS1S]
min_s1s_satisfies_xm [lemma, in Buechi.MinimalS1S]
mkFinTypeCardAtLeast3 [constructor, in Buechi.FullS1S]
mknfa [constructor, in Buechi.NFAs]
mkSG [constructor, in Buechi.FiniteSemigroups]
mkUPSeq [constructor, in Buechi.UPSequences]
MLe [constructor, in Buechi.MinimalS1S]
mmC [definition, in FinTypes.FinTypes]
MNeg [constructor, in Buechi.MinimalS1S]
MoreConnectives1 [section, in Buechi.FullS1S]
MoreConnectives2 [section, in Buechi.FullS1S]
MoreSequences [section, in Buechi.Sequences]
MoreSequences.Annotate [section, in Buechi.Sequences]
MoreSequences.Annotate.P [variable, in Buechi.Sequences]
MoreSequences.Factorize [section, in Buechi.Sequences]
MoreSequences.Factorize.P [variable, in Buechi.Sequences]
MoreSequences.InfOften [section, in Buechi.Sequences]
MoreSequences.InfOften.P [variable, in Buechi.Sequences]
MoreSequences.InfOften.P2 [variable, in Buechi.Sequences]
MoreSequences.Languages [section, in Buechi.Sequences]
MoreSequences.OmegaIteration [section, in Buechi.Sequences]
MP [definition, in Buechi.RamseyanFactorizations]
mul [definition, in Buechi.FiniteSemigroups]
mul_yields_idempotent [lemma, in Buechi.FiniteSemigroups]
mul_mult [lemma, in Buechi.FiniteSemigroups]
mul_distr [lemma, in Buechi.FiniteSemigroups]
mul_comm [lemma, in Buechi.FiniteSemigroups]
mul_step [lemma, in Buechi.FiniteSemigroups]
mul_ge_0 [lemma, in Buechi.Utils]

N

naccept_step [constructor, in Buechi.RegularLanguages]
naccept_sing [constructor, in Buechi.RegularLanguages]
naligned [definition, in Buechi.NFAs]
NatSet [abbreviation, in Buechi.FullS1S]
NatSet [abbreviation, in Buechi.FullS1S]
NatSet [abbreviation, in Buechi.NecessityRF]
nat_le_dec [instance, in FinTypes.External]
nat_eq_dec [instance, in FinTypes.External]
ncons [constructor, in Buechi.Strings]
NecessityRF [library]
Neg [constructor, in Buechi.FullS1S]
negOr [lemma, in FinTypes.BasicDefinitions]
neg_correct [lemma, in Buechi.FullS1S]
neg_merging_sym [lemma, in Buechi.RamseyanPigeonholePrinciple]
new_run_accepting [lemma, in Buechi.Buechi]
new_run_initial [lemma, in Buechi.Buechi]
new_run_valid [lemma, in Buechi.Buechi]
NFA [record, in Buechi.NFAs]
NFAs [library]
nfa_omega_iter_correct [lemma, in Buechi.Buechi]
nfa_omega_iter_accepts_aut [lemma, in Buechi.Buechi]
nfa_omega_iter [definition, in Buechi.Buechi]
nlst_step [definition, in Buechi.NFAs]
NoneElement [lemma, in FinTypes.FinTypes]
nonempty [definition, in Buechi.Strings]
NonEmptyStrings [section, in Buechi.Strings]
nonempty_substr_is_closed [lemma, in Buechi.Sequences]
nonempty_prefix_is_closed [lemma, in Buechi.Sequences]
nonempty_iff_match [lemma, in Buechi.Buechi]
notInMapCons [lemma, in FinTypes.FinTypes]
notInZero [lemma, in FinTypes.BasicDefinitions]
notright_is_left [lemma, in Buechi.Buechi]
not_in_cons [lemma, in FinTypes.External]
not_dec [instance, in FinTypes.External]
not_merge_iff [lemma, in Buechi.NecessityRF]
NStr [inductive, in Buechi.Strings]
NStrBoundedDelta [section, in Buechi.Strings]
NStrBoundedDelta.DecAndChoice [section, in Buechi.Strings]
NStrBoundedDelta.DecAndChoice' [section, in Buechi.Strings]
NStrBoundedDelta.DecAndChoice'.P [variable, in Buechi.Strings]
NStrBoundedDelta.DecAndChoice'.P' [variable, in Buechi.Strings]
NStrBoundedDelta.DecAndChoice.P [variable, in Buechi.Strings]
NStrFlatten [section, in Buechi.Strings]
NStrMap [section, in Buechi.Strings]
NStrMap.f [variable, in Buechi.Strings]
nstr_to_bnstr_delta [lemma, in Buechi.AdditiveRamsey]
nstr_to_bnstr_false [lemma, in Buechi.AdditiveRamsey]
nstr_to_bnstr_true [lemma, in Buechi.AdditiveRamsey]
nstr_to_bnstr [definition, in Buechi.AdditiveRamsey]
nstr_zip_append [lemma, in Buechi.UPSequences]
nstr_zip_nth [lemma, in Buechi.UPSequences]
nstr_zip_delta [lemma, in Buechi.UPSequences]
nstr_zip [definition, in Buechi.UPSequences]
nstr_concat_assoc [lemma, in Buechi.Sequences]
nstr_concat_sing [lemma, in Buechi.Sequences]
nstr_concat_swap [lemma, in Buechi.Sequences]
nstr_concat'_step [lemma, in Buechi.Sequences]
nstr_os_nfa_correct [lemma, in Buechi.RegularLanguages]
nstr_of_leq_delta [definition, in Buechi.Strings]
nstr_of_delta [definition, in Buechi.Strings]
nstr_finIter_length [lemma, in Buechi.Strings]
nstr_to_str_length [lemma, in Buechi.Strings]
nstr_to_str_to_nstr_idem [lemma, in Buechi.Strings]
nstr_nonempty [lemma, in Buechi.Strings]
nstr_concat_delta [lemma, in Buechi.Strings]
nstr_drop [definition, in Buechi.Strings]
nstr_flatten [definition, in Buechi.Strings]
nstr_map_concat [lemma, in Buechi.Strings]
nstr_map_nth [lemma, in Buechi.Strings]
nstr_map_length [lemma, in Buechi.Strings]
nstr_map_delta [lemma, in Buechi.Strings]
nstr_map [definition, in Buechi.Strings]
nstr_size_induction [lemma, in Buechi.Strings]
nstr_dec_eq [instance, in Buechi.Strings]
nstr_concat_last [lemma, in Buechi.Strings]
nstr_finIter_delta [lemma, in Buechi.Strings]
nstr_finIter [definition, in Buechi.Strings]
nstr_concat'_nth_snd [lemma, in Buechi.Strings]
nstr_concat'_nth_fst [lemma, in Buechi.Strings]
nstr_drop_last_nth [lemma, in Buechi.Strings]
nstr_drop_last_delta [lemma, in Buechi.Strings]
nstr_concat'_delta [lemma, in Buechi.Strings]
nstr_last_delta [lemma, in Buechi.Strings]
nstr_last [definition, in Buechi.Strings]
nstr_drop_last [definition, in Buechi.Strings]
nstr_concat' [definition, in Buechi.Strings]
nstr_concat [definition, in Buechi.Strings]
nstr_nth [definition, in Buechi.Strings]
nstr_to_str_eq [lemma, in Buechi.Strings]
nstr_to_str [definition, in Buechi.Strings]
nth_step [lemma, in Buechi.Sequences]
nth_first [lemma, in Buechi.Sequences]
nth_proper [instance, in Buechi.Sequences]
nth_first_hd [lemma, in Buechi.Sequences]
nth_step_tl [lemma, in Buechi.Sequences]
NullMul [lemma, in FinTypes.BasicDefinitions]

O

obtain_match [lemma, in Buechi.Buechi]
occurences [definition, in Buechi.Strings]
occurences_all [lemma, in Buechi.Strings]
occurences_all_instances [lemma, in Buechi.Strings]
occurences_correct [lemma, in Buechi.Strings]
occurences_dupfree [lemma, in Buechi.Strings]
occurences_bound [lemma, in Buechi.Strings]
oiter_transition [definition, in Buechi.Buechi]
OmegaIter [definition, in Buechi.Sequences]
OmegaIterProper [instance, in Buechi.Sequences]
omega_iter_map [lemma, in Buechi.Sequences]
omega_iter_sing [lemma, in Buechi.Sequences]
omega_iter_iter [lemma, in Buechi.Sequences]
omega_iter_step [lemma, in Buechi.Sequences]
omega_iter_rotate [lemma, in Buechi.Sequences]
omega_iter_correct [lemma, in Buechi.Sequences]
omega_iter [definition, in Buechi.Sequences]
once [definition, in Buechi.Sequences]
OneColorNFA [section, in Buechi.RegularLanguages]
OneColorNFA.c [variable, in Buechi.RegularLanguages]
OneColorNFA.f [variable, in Buechi.RegularLanguages]
OneColorNFA.HM [variable, in Buechi.RegularLanguages]
OneStringNFA [section, in Buechi.RegularLanguages]
OneStringNFA.x [variable, in Buechi.RegularLanguages]
one_color_nfa_correct' [lemma, in Buechi.RegularLanguages]
one_color_nfa_nonempty [lemma, in Buechi.RegularLanguages]
one_color_nfa_correct [lemma, in Buechi.RegularLanguages]
one_color_nfa_accepts_strings_of_color [lemma, in Buechi.RegularLanguages]
one_color_nfa [definition, in Buechi.RegularLanguages]
Option_Card [lemma, in FinTypes.FinTypes]
option_enum_ok [lemma, in FinTypes.FinTypes]
option_eq_dec [instance, in FinTypes.BasicDefinitions]
Or [definition, in Buechi.FullS1S]
order_g_f [lemma, in Buechi.RamseyanPigeonholePrinciple]
or_dec [instance, in FinTypes.External]
or_correct [lemma, in Buechi.FullS1S]
os_nfa_correct [lemma, in Buechi.RegularLanguages]
os_nfa_only_accepts_x [lemma, in Buechi.RegularLanguages]
os_nfa_accepts_x [lemma, in Buechi.RegularLanguages]
os_nfa [definition, in Buechi.RegularLanguages]

P

pair_eq [lemma, in Buechi.Complement]
pair_eq3 [lemma, in Buechi.Buechi]
phi_merge_correct [lemma, in Buechi.NecessityRF]
phi_merge [definition, in Buechi.NecessityRF]
phi_sum_eq_correct [lemma, in Buechi.NecessityRF]
phi_sum_eq [definition, in Buechi.NecessityRF]
phi_last_correct [lemma, in Buechi.NecessityRF]
phi_last [definition, in Buechi.NecessityRF]
phi_step_correct [lemma, in Buechi.NecessityRF]
phi_step [definition, in Buechi.NecessityRF]
phi_first_correct [lemma, in Buechi.NecessityRF]
phi_first [definition, in Buechi.NecessityRF]
phi_unique_correct [lemma, in Buechi.NecessityRF]
phi_unique [definition, in Buechi.NecessityRF]
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]
postfix [inductive, in Buechi.RegularLanguages]
postfixes [definition, in Buechi.RegularLanguages]
postfixes_contains_postfixes [lemma, in Buechi.RegularLanguages]
postfix_state [definition, in Buechi.RegularLanguages]
postfix_inversion [lemma, in Buechi.RegularLanguages]
postfix_step [constructor, in Buechi.RegularLanguages]
postfix_base [constructor, in Buechi.RegularLanguages]
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 Buechi.Utils]
predicate [projection, in FinTypes.External]
pred_xm_RP [lemma, in Buechi.NecessityRF]
prefix [definition, in Buechi.Sequences]
prefix_proper [instance, in Buechi.Sequences]
prefix_nth [lemma, in Buechi.Sequences]
prefix_length [lemma, in Buechi.Sequences]
prefix_admits_ramseyan_fac [lemma, in Buechi.RamseyanFactorizations]
prefix_of_function_length [lemma, in Buechi.FiniteSemigroups]
prefix_of_function_correct [lemma, in Buechi.FiniteSemigroups]
prefix_of_function [definition, in Buechi.FiniteSemigroups]
PreImage [definition, in Buechi.Sequences]
PreImageProper [instance, in Buechi.Sequences]
preimage_aut_correct [lemma, in Buechi.Buechi]
preimage_aut [definition, in Buechi.Buechi]
Prepend [definition, in Buechi.Sequences]
prepend [definition, in Buechi.Sequences]
PrependN [definition, in Buechi.Sequences]
PrependNProper [instance, in Buechi.Sequences]
PrependProper [instance, in Buechi.Sequences]
prepend_lang_split_position [lemma, in Buechi.Sequences]
prepend_nstr_first [lemma, in Buechi.Sequences]
prepend_nstr_assoc [lemma, in Buechi.Sequences]
prepend_nstr_nth_rest_sub [lemma, in Buechi.Sequences]
prepend_nth_rest' [lemma, in Buechi.Sequences]
prepend_nstr_nth_rest [lemma, in Buechi.Sequences]
prepend_nth_rest_sub [lemma, in Buechi.Sequences]
prepend_nth_rest [lemma, in Buechi.Sequences]
prepend_nstr_nth_first [lemma, in Buechi.Sequences]
prepend_nth_first [lemma, in Buechi.Sequences]
prepend_proper [instance, in Buechi.Sequences]
prepend_nfa_correct [lemma, in Buechi.Buechi]
prepend_aut_accepts_prepend_omega [lemma, in Buechi.Buechi]
prepend_aut_is_prepend_omega [lemma, in Buechi.Buechi]
prepend_nfa [definition, in Buechi.Buechi]
prepend_state_initial [definition, in Buechi.Buechi]
prepend_state_accepting [definition, in Buechi.Buechi]
prepend_transition [definition, in Buechi.Buechi]
preservation_FCIter [lemma, in FinTypes.FinTypes]
preservation_iter [lemma, in FinTypes.FinTypes]
preservation_step [lemma, in FinTypes.FinTypes]
ProdCount [lemma, in FinTypes.FinTypes]
prodLists [definition, in FinTypes.BasicDefinitions]
Prod_Card [lemma, in FinTypes.FinTypes]
prod_enum_ok [lemma, in FinTypes.FinTypes]
prod_nil [lemma, in FinTypes.BasicDefinitions]
prod_eq_dec [instance, in FinTypes.BasicDefinitions]
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]
purify [lemma, in FinTypes.BasicDefinitions]
P1 [definition, in Buechi.NecessityRF]
P2 [definition, in Buechi.NecessityRF]
P3 [definition, in Buechi.NecessityRF]

Q

quasi_run_implies_accepting [lemma, in Buechi.Buechi]

R

RA [definition, in Buechi.AdditiveRamsey]
RamseyanFactorizations [section, in Buechi.RamseyanFactorizations]
RamseyanFactorizations [library]
RamseyanFactorizations.DefinitionAndBasics [section, in Buechi.RamseyanFactorizations]
RamseyanPigeonholePrinciple [section, in Buechi.RamseyanPigeonholePrinciple]
RamseyanPigeonholePrinciple [library]
RamseyanPigeonholePrinciple.Merging [section, in Buechi.RamseyanPigeonholePrinciple]
RamseyanPigeonholePrinciple.Merging.sigma [variable, in Buechi.RamseyanPigeonholePrinciple]
ramseyan_fac_combine [lemma, in Buechi.RamseyanFactorizations]
RamseyFac_iff_RamseyFac' [lemma, in Buechi.RamseyanFactorizations]
ramsey_fac_iff_homogenous [lemma, in Buechi.AdditiveRamsey]
ramsey_nfa_correct [lemma, in Buechi.NecessityRF]
ramsey_nfa [definition, in Buechi.NecessityRF]
ramsey_nfa_color_correct [lemma, in Buechi.NecessityRF]
ramsey_nfa_color [definition, in Buechi.NecessityRF]
RA_implies_RF [lemma, in Buechi.AdditiveRamsey]
RegularLanguages [section, in Buechi.RegularLanguages]
RegularLanguages [library]
relation [projection, in FinTypes.External]
rem [definition, in FinTypes.External]
Removal [section, in FinTypes.External]
Removal.X [variable, in FinTypes.External]
remove_loops_nstr [lemma, in Buechi.NFAs]
remove_loops [lemma, in Buechi.NFAs]
remove_loop [lemma, in Buechi.NFAs]
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_injection_eq [lemma, in Buechi.MinimalS1S]
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]
ResultsFullS1S [section, in Buechi.FullS1S]
ResultsFullS1S.ASSemantics [section, in Buechi.FullS1S]
ResultsFullS1S.UPSemantics [section, in Buechi.FullS1S]
revert_drop [lemma, in Buechi.Sequences]
revert_nstr_prepend [lemma, in Buechi.Sequences]
revert_prepend [lemma, in Buechi.Sequences]
RF [definition, in Buechi.RamseyanFactorizations]
RF_implies_FX [lemma, in Buechi.FullS1S]
RF_implies_RA [lemma, in Buechi.AdditiveRamsey]
RF_implies_RP [lemma, in Buechi.RamseyanPigeonholePrinciple]
RF_implies_IP [lemma, in Buechi.RamseyanFactorizations]
RF_impl_IP_impl_MP [section, in Buechi.RamseyanFactorizations]
RF' [definition, in Buechi.RamseyanFactorizations]
rho' [definition, in Buechi.Buechi]
rho'_accepts [lemma, in Buechi.Buechi]
rho'_firsts [lemma, in Buechi.Buechi]
rightResult [lemma, in FinTypes.FinTypes]
RP [definition, in Buechi.RamseyanPigeonholePrinciple]
RPc [definition, in Buechi.RamseyanPigeonholePrinciple]
RPc_holds [lemma, in Buechi.RamseyanPigeonholePrinciple]
RPc_sigma [definition, in Buechi.RamseyanPigeonholePrinciple]
RPIffRF [section, in Buechi.RamseyanPigeonholePrinciple]
RPIffRF.RPImpliesRF [section, in Buechi.RamseyanPigeonholePrinciple]
RPIffRF.RPImpliesRF.H [variable, in Buechi.RamseyanPigeonholePrinciple]
RP_implies_RF [lemma, in Buechi.RamseyanPigeonholePrinciple]
rp_implies_inf_merging_pos [lemma, in Buechi.RamseyanPigeonholePrinciple]
RP_implies_IP [lemma, in Buechi.RamseyanPigeonholePrinciple]
RP_sigma [definition, in Buechi.RamseyanPigeonholePrinciple]
RP_iff_RPc_pred [lemma, in Buechi.NecessityRF]
Run [definition, in Buechi.NFAs]
Run [abbreviation, in Buechi.Buechi]

S

saccepting_ind_iff_snaccepting_ind [lemma, in Buechi.RegularLanguages]
saccepting_ind [inductive, in Buechi.RegularLanguages]
safe [inductive, in Buechi.Utils]
safeB [constructor, in Buechi.Utils]
safeS [constructor, in Buechi.Utils]
safe_dclosed [lemma, in Buechi.Utils]
SAll [definition, in Buechi.FullS1S]
same_color_same_accepting_quasi [lemma, in Buechi.Complement]
same_color_transforms_accepting [lemma, in Buechi.Complement]
same_color_transforms [lemma, in Buechi.Complement]
sat [definition, in Buechi.FullS1S]
sat [definition, in Buechi.MinimalS1S]
satisfaction_sat_xm [lemma, in Buechi.MinimalS1S]
satisfies [definition, in Buechi.FullS1S]
satisfies [definition, in Buechi.MinimalS1S]
satisfies_fun_extensional_bi [lemma, in Buechi.FullS1S]
satisfies_fun_extensional [lemma, in Buechi.FullS1S]
satisfies_fun [definition, in Buechi.FullS1S]
satisfies_proper [instance, in Buechi.MinimalS1S]
satisfies_extensional [lemma, in Buechi.MinimalS1S]
sat_up_obtain [lemma, in Buechi.MinimalS1S]
sat_iff_aut_non_empty [lemma, in Buechi.MinimalS1S]
sat_xm_exists_not_merging [lemma, in Buechi.NecessityRF]
sat_xm_exists_index_inf_merging [lemma, in Buechi.NecessityRF]
sat_xm_exists_merging [lemma, in Buechi.NecessityRF]
sat_xm_nat_dec_exists [lemma, in Buechi.NecessityRF]
sat_xm_satis [instance, in Buechi.NecessityRF]
sat_xm_iff [lemma, in Buechi.Utils]
sat_xm_proper [instance, in Buechi.Utils]
sat_xm_from_dec [instance, in Buechi.Utils]
sat_xm_not [instance, in Buechi.Utils]
sat_xm_or [instance, in Buechi.Utils]
sat_xm_and [instance, in Buechi.Utils]
sat_xm [definition, in Buechi.Utils]
scons [projection, in Buechi.Sequences]
scons_correct [lemma, in Buechi.Sequences]
scons_proper [instance, in Buechi.Sequences]
Seq [projection, in Buechi.Sequences]
SeqDummy [instance, in Buechi.Sequences]
SeqInstances [section, in Buechi.UPSequences]
SeqInstances.BaseUP [section, in Buechi.UPSequences]
SeqInstances.BaseUP.X [variable, in Buechi.UPSequences]
SeqInstances.NStrZip [section, in Buechi.UPSequences]
SeqInstances.UPMap [section, in Buechi.UPSequences]
SeqInstances.UPMap.X [variable, in Buechi.UPSequences]
SeqInstances.UPMap.Y [variable, in Buechi.UPSequences]
SeqInstances.UPZip [section, in Buechi.UPSequences]
SeqInstances.UPZip.X [variable, in Buechi.UPSequences]
SeqInstances.UPZip.Y [variable, in Buechi.UPSequences]
SeqInstances.ZipEqUP [section, in Buechi.UPSequences]
SeqInstances.ZipEqUP.UPEqualizePrefix [section, in Buechi.UPSequences]
SeqNStrDummy [instance, in Buechi.Sequences]
Sequence [instance, in Buechi.Sequences]
Sequences [section, in Buechi.Sequences]
Sequences [library]
SequenceWithConst [instance, in Buechi.Sequences]
SequenceWithZipMap [instance, in Buechi.Sequences]
seq_implies_function [lemma, in Buechi.FullS1S]
seq_factorize [definition, in Buechi.Sequences]
seq_flatten [definition, in Buechi.Sequences]
seq_nth [lemma, in Buechi.Sequences]
seq_equiv_equiv [instance, in Buechi.Sequences]
seq_to_sets_nth [lemma, in Buechi.NecessityRF]
seq_to_sets [definition, in Buechi.NecessityRF]
seq_irun [definition, in Buechi.Buechi]
set_map_correct [lemma, in Buechi.FinSets]
set_map [definition, in Buechi.FinSets]
set_eq' [lemma, in Buechi.FinSets]
set_eq [lemma, in Buechi.FinSets]
set_mem_proper [instance, in Buechi.MinimalS1S]
set_mem [definition, in Buechi.MinimalS1S]
SEx [constructor, in Buechi.FullS1S]
sigT_enum_ok [lemma, in FinTypes.FinTypes]
sigT_proj2_fun [lemma, in FinTypes.BasicDefinitions]
sigT_proj1_fun [lemma, in FinTypes.BasicDefinitions]
Sing [definition, in Buechi.FullS1S]
sing [constructor, in Buechi.Strings]
singleton [definition, in Buechi.FinSets]
SingletonNFA [section, in Buechi.RegularLanguages]
SingletonNFA.P [variable, in Buechi.RegularLanguages]
singletonSet [definition, in Buechi.FullS1S]
singletonSetCorrect1 [lemma, in Buechi.FullS1S]
singletonSetCorrect2 [lemma, in Buechi.FullS1S]
singleton_correct' [lemma, in Buechi.FinSets]
singleton_correct [lemma, in Buechi.FinSets]
singleton_is_singleton [lemma, in Buechi.FullS1S]
singleton_iff [lemma, in Buechi.FullS1S]
singleton_nfa_nstr_correct [lemma, in Buechi.RegularLanguages]
singleton_nfa_correct [lemma, in Buechi.RegularLanguages]
singleton_lang [definition, in Buechi.RegularLanguages]
singleton_nfa [definition, in Buechi.RegularLanguages]
sing_correct [lemma, in Buechi.FullS1S]
sing_equiv [lemma, in Buechi.FullS1S]
size_induction [lemma, in FinTypes.External]
slanguage_ind [definition, in Buechi.RegularLanguages]
snaccepting_ind [inductive, in Buechi.RegularLanguages]
snlanguage_ind_iff_slanguage_ind [lemma, in Buechi.RegularLanguages]
snlanguage_ind [definition, in Buechi.RegularLanguages]
SomeElement [lemma, in FinTypes.FinTypes]
split_string_eq [lemma, in Buechi.UPSequences]
split_transforms_accepting [lemma, in Buechi.NFAs]
split_transforms [lemma, in Buechi.NFAs]
state [projection, in Buechi.NFAs]
states_do_not_mix [lemma, in Buechi.Buechi]
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]
Str [abbreviation, in Buechi.Strings]
Streicher_K [lemma, in FinTypes.BasicDefinitions]
StrictMonotonicity [section, in Buechi.Utils]
strict_bounded_exist [instance, in Buechi.Utils]
Strings [library]
strings_of_color_accepted_by_one_color_nfa [lemma, in Buechi.RegularLanguages]
string_fixed_length_cc' [lemma, in Buechi.Strings]
string_bounded_length_cc [lemma, in Buechi.Strings]
string_fixed_length_cc [lemma, in Buechi.Strings]
StrToNStr [section, in Buechi.Strings]
str_nth_nstr' [lemma, in Buechi.Strings]
str_nth_nstr [lemma, in Buechi.Strings]
str_nth [definition, in Buechi.Strings]
str_to_nstr_idem' [lemma, in Buechi.Strings]
str_to_nstr_idem [lemma, in Buechi.Strings]
str_to_nstr [definition, in Buechi.Strings]
subset [definition, in Buechi.FinSets]
subset [definition, in Buechi.FullS1S]
subset_eq [lemma, in Buechi.FinSets]
subset_proper [instance, in Buechi.FullS1S]
substr [definition, in Buechi.Sequences]
substr_flatten [lemma, in Buechi.AdditiveRamsey]
substr_proper [instance, in Buechi.Sequences]
substr_nth [lemma, in Buechi.Sequences]
substr_length [lemma, in Buechi.Sequences]
substr' [definition, in Buechi.Sequences]
substr'_split [lemma, in Buechi.Sequences]
substr'_prepend' [lemma, in Buechi.Sequences]
substr'_nth [lemma, in Buechi.Sequences]
substr'_delta [lemma, in Buechi.Sequences]
substr'_proper [instance, in Buechi.Sequences]
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]
suffixsums_aut_trans_correct [lemma, in Buechi.NecessityRF]
suffixsums_aut [definition, in Buechi.NecessityRF]
suffixsums_aut_trans [definition, in Buechi.NecessityRF]
SUM [definition, in Buechi.FiniteSemigroups]
SumCard [lemma, in FinTypes.FinTypes]
sum_enum_ok [lemma, in FinTypes.FinTypes]
sum_eq_dec [instance, in FinTypes.BasicDefinitions]
sum_occurences [definition, in Buechi.Strings]
SUM_flatten [lemma, in Buechi.FiniteSemigroups]
SUM_is_homomorphism [lemma, in Buechi.FiniteSemigroups]
SUM_concat [lemma, in Buechi.FiniteSemigroups]
sum_aut_trans_correct [lemma, in Buechi.NecessityRF]
sum_aut [definition, in Buechi.NecessityRF]
sum_aut_trans [definition, in Buechi.NecessityRF]
surjective [definition, in FinTypes.BasicDefinitions]
surjectiveApply [lemma, in FinTypes.BasicDefinitions]
surj_sub [lemma, in FinTypes.FinTypes]
swap_sum [definition, in Buechi.Buechi]
switch_from_V_to_W [lemma, in Buechi.Buechi]
s_monotone_order_preserving [lemma, in Buechi.Utils]
s_monotone_order_preserving' [lemma, in Buechi.Utils]
s_monotone_bound [lemma, in Buechi.Utils]
s_monotone [definition, in Buechi.Utils]
s1s_DM_exist_neg [lemma, in Buechi.FullS1S]
s1s_DM_forall_neg [lemma, in Buechi.FullS1S]
s1s_DM_neg_and [lemma, in Buechi.FullS1S]
s1s_impl [definition, in Buechi.FullS1S]
s1s_coincidence_bi [lemma, in Buechi.FullS1S]
s1s_coincidence' [lemma, in Buechi.FullS1S]
s1s_coincidence [lemma, in Buechi.FullS1S]

T

tau_transforms_zip [lemma, in Buechi.Buechi]
Test [section, in FinTypes.FinTypes]
test_destruct_annotate [lemma, in Buechi.Sequences]
Test.X [variable, in FinTypes.FinTypes]
Test.Y [variable, in FinTypes.FinTypes]
# _ [notation, in FinTypes.FinTypes]
tl [projection, in Buechi.Sequences]
tl_preserves_encodes_fact [lemma, in Buechi.AdditiveRamsey]
tl_proper [instance, in Buechi.Sequences]
tl_correct [projection, in Buechi.Sequences]
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]
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]
toMinMSO [definition, in Buechi.FullS1S]
toMinMSO_correct [lemma, in Buechi.FullS1S]
toMinMSO' [definition, in Buechi.FullS1S]
toOptionList [definition, in FinTypes.BasicDefinitions]
top [definition, in Buechi.FullS1S]
top_correct [lemma, in Buechi.FullS1S]
toright [definition, in Buechi.Buechi]
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 [lemma, in Buechi.Complement]
totality_up [lemma, in Buechi.Complement]
toV1 [abbreviation, in Buechi.FullS1S]
toV2 [abbreviation, in Buechi.FullS1S]
to_min_s1s_complete [lemma, in Buechi.FullS1S]
to_min_s1s_correct [lemma, in Buechi.FullS1S]
transforms [inductive, in Buechi.NFAs]
TransformsRelations [section, in Buechi.NFAs]
TransformsRelations.aut [variable, in Buechi.NFAs]
TransformsRelations.Decidability [section, in Buechi.NFAs]
_ =!=> _ on _ [notation, in Buechi.NFAs]
_ ===> _ on _ [notation, in Buechi.NFAs]
transforms_accepting_run_cc [lemma, in Buechi.NFAs]
transforms_run_cc [lemma, in Buechi.NFAs]
transforms_accepting_equiv [lemma, in Buechi.NFAs]
transforms_iff_valid_path [lemma, in Buechi.NFAs]
transforms_equiv [lemma, in Buechi.NFAs]
transforms_accepting_iff [lemma, in Buechi.NFAs]
transforms_accepting_concat [lemma, in Buechi.NFAs]
transforms_concat [lemma, in Buechi.NFAs]
transforms_accepting_inv [lemma, in Buechi.NFAs]
transforms_inv [lemma, in Buechi.NFAs]
transforms_accepting_implies_transform [lemma, in Buechi.NFAs]
transforms_accepting [inductive, in Buechi.NFAs]
transforms_not_accepting_is_accepted [lemma, in Buechi.Buechi]
transforms_not_accepting_is_accepted' [lemma, in Buechi.Buechi]
transforms_not_accepting [inductive, in Buechi.Buechi]
transforms_accepting_image_aut_transforms_accepting_aut [lemma, in Buechi.Buechi]
transforms_image_aut_transforms_aut [lemma, in Buechi.Buechi]
transition [projection, in Buechi.NFAs]
TransitionGraph [section, in Buechi.NFAs]
transition_dec_public [instance, in Buechi.NFAs]
transition_dec [projection, in Buechi.NFAs]
transition_from_none [lemma, in Buechi.NecessityRF]
trans_accepting_step [constructor, in Buechi.NFAs]
trans_accepting_base [constructor, in Buechi.NFAs]
trans_step [constructor, in Buechi.NFAs]
trans_base [constructor, in Buechi.NFAs]
trans_not_step [constructor, in Buechi.Buechi]
trans_not_base [constructor, in Buechi.Buechi]
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

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 Buechi.UPSequences]
union [definition, in Buechi.FinSets]
union [definition, in Buechi.Buechi]
union_assoc [lemma, in Buechi.FinSets]
union_correct [lemma, in Buechi.FinSets]
union_correct [lemma, in Buechi.Buechi]
union_symmetric [lemma, in Buechi.Buechi]
union_symmetric_acc [lemma, in Buechi.Buechi]
union_accepting [definition, in Buechi.Buechi]
union_initial [definition, in Buechi.Buechi]
union_transition [definition, in Buechi.Buechi]
unit_enum_ok [lemma, in FinTypes.FinTypes]
unit_eq_dec [instance, in FinTypes.BasicDefinitions]
universal_language [definition, in Buechi.Utils]
univ_aut_scorrect [lemma, in Buechi.RegularLanguages]
univ_aut [definition, in Buechi.NFAs]
univ_aut_correct [lemma, in Buechi.Buechi]
unwrp [projection, in Buechi.Sequences]
UPBuechiAbstractAutomaton [instance, in Buechi.MinimalS1S]
update_equiv_apart' [lemma, in Buechi.FullS1S]
update_equiv_apart [lemma, in Buechi.FullS1S]
update_second_order [lemma, in Buechi.FullS1S]
update_first_order [lemma, in Buechi.FullS1S]
update_head_hd_correct [lemma, in Buechi.AdditiveRamsey]
update_true_mem [lemma, in Buechi.AdditiveRamsey]
update_false_mem [lemma, in Buechi.AdditiveRamsey]
update_head [definition, in Buechi.AdditiveRamsey]
UPSeq [record, in Buechi.UPSequences]
UPSequence [instance, in Buechi.UPSequences]
UPSequences [library]
UPWithConst [instance, in Buechi.UPSequences]
UPWithZipMap [instance, in Buechi.UPSequences]
up_zip_correct [lemma, in Buechi.UPSequences]
up_zip [definition, in Buechi.UPSequences]
up_iter_loop_loop_length [lemma, in Buechi.UPSequences]
up_iter_loop_prefix [lemma, in Buechi.UPSequences]
up_iter_loop_correct [lemma, in Buechi.UPSequences]
up_iter_loop [definition, in Buechi.UPSequences]
up_eq_zip_correct [lemma, in Buechi.UPSequences]
up_eq_zip [definition, in Buechi.UPSequences]
up_prefix_correct [lemma, in Buechi.UPSequences]
up_map_correct [lemma, in Buechi.UPSequences]
up_map [definition, in Buechi.UPSequences]
up_nth_correct [lemma, in Buechi.UPSequences]
up_equiv [lemma, in Buechi.UPSequences]
up_cons_unfold [lemma, in Buechi.UPSequences]
up_drop_correct [lemma, in Buechi.UPSequences]
up_tl_correct [lemma, in Buechi.UPSequences]
up_hd_correct [lemma, in Buechi.UPSequences]
up_const_correct [lemma, in Buechi.UPSequences]
up_const [definition, in Buechi.UPSequences]
up_cons [definition, in Buechi.UPSequences]
up_tl [definition, in Buechi.UPSequences]
up_hd [definition, in Buechi.UPSequences]
up_loop [projection, in Buechi.UPSequences]
up_prefix [projection, in Buechi.UPSequences]
up_admits_ramseyan_fac [lemma, in Buechi.RamseyanFactorizations]
Utils [library]

V

V [projection, in Buechi.FullS1S]
valid_path_remove [lemma, in Buechi.NFAs]
valid_run_transforms_everywhere [lemma, in Buechi.NFAs]
valid_run_is_path_everywhere [lemma, in Buechi.NFAs]
valid_run_cons [lemma, in Buechi.NFAs]
valid_run_drop [lemma, in Buechi.NFAs]
valid_run_tl [lemma, in Buechi.NFAs]
valid_run_proper [instance, in Buechi.NFAs]
valid_run_extensional [lemma, in Buechi.NFAs]
valid_path_length [lemma, in Buechi.NFAs]
valid_path_nth [lemma, in Buechi.NFAs]
valid_path_step [constructor, in Buechi.NFAs]
valid_path_base [constructor, in Buechi.NFAs]
valid_path [inductive, in Buechi.NFAs]
valid_run [definition, in Buechi.NFAs]
Var [definition, in Buechi.FullS1S]
vector [definition, in FinTypes.FinTypes]
vectorise [definition, in FinTypes.FinTypes]
vectorise_apply_inverse [lemma, in FinTypes.FinTypes]
vectorise_apply_inverse' [lemma, in FinTypes.FinTypes]
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 Buechi.Utils]
VW_part_of_complement_iff [lemma, in Buechi.Complement]
VW_aut_correct [lemma, in Buechi.Complement]
VW_aut [definition, in Buechi.Complement]
V_1 [instance, in Buechi.NecessityRF]
V_2 [definition, in Buechi.NecessityRF]

W

WithConst [record, in Buechi.Sequences]
WithConstLemmas [section, in Buechi.Sequences]
WithZipMap [record, in Buechi.Sequences]
WithZipMapLemmas [section, in Buechi.Sequences]
WithZipMapLemmas.BigZip [section, in Buechi.Sequences]
wrap [definition, in Buechi.Sequences]
wrap_correct [lemma, in Buechi.Sequences]
wrp [constructor, in Buechi.Sequences]
WSeq [record, in Buechi.Sequences]

X

X [definition, in Buechi.NecessityRF]
x1 [projection, in Buechi.FullS1S]
x2 [projection, in Buechi.FullS1S]
x3 [projection, in Buechi.FullS1S]

Y

Y [definition, in Buechi.NecessityRF]

Z

zip [projection, in Buechi.Sequences]
zipFinTypes [definition, in Buechi.Sequences]
zip_map_fst [lemma, in Buechi.Sequences]
zip_drop [lemma, in Buechi.Sequences]
zip_nth [lemma, in Buechi.Sequences]
zip_proper [instance, in Buechi.Sequences]
zip_correct [projection, in Buechi.Sequences]

other

_ ** _ (EqTypeScope) [notation, in FinTypes.BasicDefinitions]
_ === _ [notation, in FinTypes.External]
_ <<= _ [notation, in FinTypes.External]
_ el _ [notation, in FinTypes.External]
_ mem _ [notation, in Buechi.FinSets]
_ ==>2 _ [notation, in Buechi.FullS1S]
_ \/2 _ [notation, in Buechi.FullS1S]
_ <=2 _ [notation, in Buechi.FullS1S]
_ elS _ [notation, in Buechi.FullS1S]
_ # _ |== _ [notation, in Buechi.FullS1S]
_ [ _ := _ ] [notation, in Buechi.FullS1S]
_ /\2 _ [notation, in Buechi.FullS1S]
_ el2 _ [notation, in Buechi.FullS1S]
_ <2 _ [notation, in Buechi.FullS1S]
_ o' _ [notation, in Buechi.Sequences]
_ o _ [notation, in Buechi.Sequences]
_ ^00 [notation, in Buechi.Sequences]
_ +++ _ [notation, in Buechi.Sequences]
_ == _ [notation, in Buechi.Sequences]
_ ::: _ [notation, in Buechi.Sequences]
_ ^ _ [notation, in FinTypes.FinTypes]
_ --> _ [notation, in FinTypes.FinTypes]
_ (+) _ [notation, in FinTypes.FinTypes]
_ (x) _ [notation, in FinTypes.FinTypes]
_ ** _ [notation, in FinTypes.BasicDefinitions]
_ /\0 _ [notation, in Buechi.MinimalS1S]
_ <<=0 _ [notation, in Buechi.MinimalS1S]
_ <0 _ [notation, in Buechi.MinimalS1S]
_ =!=> _ on _ [notation, in Buechi.NFAs]
_ ===> _ on _ [notation, in Buechi.NFAs]
_ ^^ _ [notation, in Buechi.Utils]
_ ^$~ [notation, in Buechi.Utils]
_ /$\ _ [notation, in Buechi.Utils]
_ \$/ _ [notation, in Buechi.Utils]
_ =$= _ [notation, in Buechi.Utils]
_ <$= _ [notation, in Buechi.Utils]
all1 _ , _ [notation, in Buechi.FullS1S]
all2 _ , _ [notation, in Buechi.FullS1S]
AND { _ | _ } _ [notation, in Buechi.FullS1S]
eq_dec _ [notation, in FinTypes.External]
ex0 _ , _ [notation, in Buechi.MinimalS1S]
ex1 _ , _ [notation, in Buechi.FullS1S]
ex2 _ , _ [notation, in Buechi.FullS1S]
L_NR [notation, in Buechi.RegularLanguages]
L_R [notation, in Buechi.RegularLanguages]
L_B [notation, in Buechi.Buechi]
OR { _ | _ } _ [notation, in Buechi.FullS1S]
! _ [notation, in Buechi.Strings]
# _ [notation, in FinTypes.FinTypes]
? _ [notation, in FinTypes.FinTypes]
?? _ [notation, in FinTypes.BasicDefinitions]
{} [notation, in Buechi.Utils]
| _ | [notation, in FinTypes.External]
~0 _ [notation, in Buechi.MinimalS1S]
~2 _ [notation, in Buechi.FullS1S]

---

Notation Index

B

_ +++ _ [in Buechi.Sequences]
L_B [in Buechi.Buechi]

C

{[ _ ]} [in Buechi.Complement]

F

_ mem _ [in Buechi.FinSets]
<\ _ |> [in Buechi.FullS1S]
<| _ , _ /> [in Buechi.FullS1S]
[ _ ] [in Buechi.FullS1S]
<< _ , _ >> [in Buechi.FullS1S]
_ |= _ [in Buechi.FullS1S]
_ # _ |== _ [in Buechi.FullS1S]
_ [ _ := _ ] [in Buechi.FullS1S]
_ elS _ [in Buechi.FullS1S]

M

_ |= _ [in Buechi.MinimalS1S]

T

# _ [in FinTypes.FinTypes]
_ =!=> _ on _ [in Buechi.NFAs]
_ ===> _ on _ [in Buechi.NFAs]

other

_ ** _ (EqTypeScope) [in FinTypes.BasicDefinitions]
_ === _ [in FinTypes.External]
_ <<= _ [in FinTypes.External]
_ el _ [in FinTypes.External]
_ mem _ [in Buechi.FinSets]
_ ==>2 _ [in Buechi.FullS1S]
_ \/2 _ [in Buechi.FullS1S]
_ <=2 _ [in Buechi.FullS1S]
_ elS _ [in Buechi.FullS1S]
_ # _ |== _ [in Buechi.FullS1S]
_ [ _ := _ ] [in Buechi.FullS1S]
_ /\2 _ [in Buechi.FullS1S]
_ el2 _ [in Buechi.FullS1S]
_ <2 _ [in Buechi.FullS1S]
_ o' _ [in Buechi.Sequences]
_ o _ [in Buechi.Sequences]
_ ^00 [in Buechi.Sequences]
_ +++ _ [in Buechi.Sequences]
_ == _ [in Buechi.Sequences]
_ ::: _ [in Buechi.Sequences]
_ ^ _ [in FinTypes.FinTypes]
_ --> _ [in FinTypes.FinTypes]
_ (+) _ [in FinTypes.FinTypes]
_ (x) _ [in FinTypes.FinTypes]
_ ** _ [in FinTypes.BasicDefinitions]
_ /\0 _ [in Buechi.MinimalS1S]
_ <<=0 _ [in Buechi.MinimalS1S]
_ <0 _ [in Buechi.MinimalS1S]
_ =!=> _ on _ [in Buechi.NFAs]
_ ===> _ on _ [in Buechi.NFAs]
_ ^^ _ [in Buechi.Utils]
_ ^$~ [in Buechi.Utils]
_ /$\ _ [in Buechi.Utils]
_ \$/ _ [in Buechi.Utils]
_ =$= _ [in Buechi.Utils]
_ <$= _ [in Buechi.Utils]
all1 _ , _ [in Buechi.FullS1S]
all2 _ , _ [in Buechi.FullS1S]
AND { _ | _ } _ [in Buechi.FullS1S]
eq_dec _ [in FinTypes.External]
ex0 _ , _ [in Buechi.MinimalS1S]
ex1 _ , _ [in Buechi.FullS1S]
ex2 _ , _ [in Buechi.FullS1S]
L_NR [in Buechi.RegularLanguages]
L_R [in Buechi.RegularLanguages]
L_B [in Buechi.Buechi]
OR { _ | _ } _ [in Buechi.FullS1S]
! _ [in Buechi.Strings]
# _ [in FinTypes.FinTypes]
? _ [in FinTypes.FinTypes]
?? _ [in FinTypes.BasicDefinitions]
{} [in Buechi.Utils]
| _ | [in FinTypes.External]
~0 _ [in Buechi.MinimalS1S]
~2 _ [in Buechi.FullS1S]

---

Variable Index

A

AXImpliesRP.AutAll.P [in Buechi.NecessityRF]
AXImpliesRP.ax [in Buechi.NecessityRF]
AXImpliesRP.ExAut.P [in Buechi.NecessityRF]

B

Buechi.BuechiAutomaton.aut [in Buechi.Buechi]
Buechi.ImageNFA.aut [in Buechi.Buechi]
Buechi.ImageNFA.f [in Buechi.Buechi]
Buechi.Intersection.aut_2 [in Buechi.Buechi]
Buechi.Intersection.aut_1 [in Buechi.Buechi]
Buechi.Intersection.IRun.F1 [in Buechi.Buechi]
Buechi.Intersection.IRun.F2 [in Buechi.Buechi]
Buechi.Intersection.IRun.rho_2 [in Buechi.Buechi]
Buechi.Intersection.IRun.rho_1 [in Buechi.Buechi]
Buechi.Intersection.IRun.sigma [in Buechi.Buechi]
Buechi.Match.aut [in Buechi.Buechi]
Buechi.NFAOmegaIteration.aut [in Buechi.Buechi]
Buechi.PreImageNFA.aut [in Buechi.Buechi]
Buechi.PreImageNFA.f [in Buechi.Buechi]
Buechi.PrependNFA.aut_2 [in Buechi.Buechi]
Buechi.PrependNFA.aut_1 [in Buechi.Buechi]
Buechi.QuasiRun.aut [in Buechi.Buechi]
Buechi.QuasiRun.QuasiRunImpliesAccepting.Acc [in Buechi.Buechi]
Buechi.QuasiRun.QuasiRunImpliesAccepting.rho [in Buechi.Buechi]
Buechi.QuasiRun.QuasiRunImpliesAccepting.tau [in Buechi.Buechi]
Buechi.Union.Def.aut_2 [in Buechi.Buechi]
Buechi.Union.Def.aut_1 [in Buechi.Buechi]

C

Cardinality.X [in FinTypes.External]
Complement.aut [in Buechi.Complement]

D

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.P [in Buechi.Strings]
FilterLemmas.Q [in Buechi.Strings]
FilterLemmas.X [in FinTypes.External]
FiniteClosureIteration.step [in FinTypes.FinTypes]
FiniteClosureIteration.step_dec [in FinTypes.FinTypes]
FiniteClosureIteration.X [in FinTypes.FinTypes]
FiniteSets.X [in Buechi.FinSets]
FirstGeq.f [in Buechi.Utils]
FirstGeq.FirstGeqExists.L [in Buechi.Utils]
FirstGeq.FirstGeq.F [in Buechi.Utils]
FirstGeq.FirstGeq.L [in Buechi.Utils]
FirstGeq.P [in Buechi.Utils]
First.p [in Buechi.Utils]
First.p_dec [in Buechi.Utils]
Fixedpoints.f [in FinTypes.FinTypes]
Fixedpoints.X [in FinTypes.FinTypes]
FullS1S.Coincidence.FVar [in Buechi.FullS1S]
FullS1S.Coincidence.SVar [in Buechi.FullS1S]
FullS1S.ConvertInterpretations.V [in Buechi.FullS1S]
FullS1S.ReduceFullS1S_to_MinS1S.SVar [in Buechi.FullS1S]
FullS1S.ReduceFullS1S_to_MinS1S.FVar [in Buechi.FullS1S]
FXImpliesRP.MSO_XM [in Buechi.NecessityRF]

I

Inclusion.X [in FinTypes.External]

L

LanguageLemmata.L [in Buechi.Utils]
LanguageLemmata.L_2 [in Buechi.Utils]
LanguageLemmata.L_1 [in Buechi.Utils]
LanguageLemmata.X [in Buechi.Utils]
Languages.X [in Buechi.Utils]

M

Membership.X [in FinTypes.External]
MinS1SToBuechi.X [in Buechi.MinimalS1S]
MinS1SToBuechi.Y [in Buechi.MinimalS1S]
MoreSequences.Annotate.P [in Buechi.Sequences]
MoreSequences.Factorize.P [in Buechi.Sequences]
MoreSequences.InfOften.P [in Buechi.Sequences]
MoreSequences.InfOften.P2 [in Buechi.Sequences]

N

NStrBoundedDelta.DecAndChoice'.P [in Buechi.Strings]
NStrBoundedDelta.DecAndChoice'.P' [in Buechi.Strings]
NStrBoundedDelta.DecAndChoice.P [in Buechi.Strings]
NStrMap.f [in Buechi.Strings]

O

OneColorNFA.c [in Buechi.RegularLanguages]
OneColorNFA.f [in Buechi.RegularLanguages]
OneColorNFA.HM [in Buechi.RegularLanguages]
OneStringNFA.x [in Buechi.RegularLanguages]

P

PowerRep.X [in FinTypes.External]

R

RamseyanPigeonholePrinciple.Merging.sigma [in Buechi.RamseyanPigeonholePrinciple]
Removal.X [in FinTypes.External]
RPIffRF.RPImpliesRF.H [in Buechi.RamseyanPigeonholePrinciple]

S

SeqInstances.BaseUP.X [in Buechi.UPSequences]
SeqInstances.UPMap.X [in Buechi.UPSequences]
SeqInstances.UPMap.Y [in Buechi.UPSequences]
SeqInstances.UPZip.X [in Buechi.UPSequences]
SeqInstances.UPZip.Y [in Buechi.UPSequences]
SingletonNFA.P [in Buechi.RegularLanguages]

T

Test.X [in FinTypes.FinTypes]
Test.Y [in FinTypes.FinTypes]
TransformsRelations.aut [in Buechi.NFAs]

U

Undup.X [in FinTypes.External]

---

Library Index

A

AdditiveRamsey

B

BasicDefinitions
Buechi

C

Complement

E

External

F

FiniteSemigroups
FinSets
FinTypes
FullS1S

M

MinimalS1S

N

NecessityRF
NFAs

R

RamseyanFactorizations
RamseyanPigeonholePrinciple
RegularLanguages

S

Sequences
Strings

U

UPSequences
Utils

---

Lemma Index

A

accepted_strings_transforms [in Buechi.Buechi]
accepted_strings_transforms' [in Buechi.Buechi]
accepting_quasi_run_iff_accepts [in Buechi.Buechi]
accepting_implies_quasirun [in Buechi.Buechi]
accepting_extensional [in Buechi.Buechi]
AC_equiv_RF [in Buechi.NecessityRF]
AC_implies_AX [in Buechi.NecessityRF]
addGamma_is_associative [in Buechi.Complement]
additive_to_substr' [in Buechi.AdditiveRamsey]
admits_ramseyan_fac_iff_idem_ramseyan_fac [in Buechi.RamseyanFactorizations]
allSub [in FinTypes.FinTypes]
all_aut_correct [in Buechi.NecessityRF]
all1_correct [in Buechi.FullS1S]
all2_correct [in Buechi.FullS1S]
and_correct [in Buechi.FullS1S]
annotate_correct [in Buechi.Sequences]
appendNil [in FinTypes.BasicDefinitions]
apply_vectorise_inverse [in FinTypes.FinTypes]
autU_accepted_by_aut1 [in Buechi.Buechi]
aut_lang_sat_xm [in Buechi.MinimalS1S]
aut_forall_sums_different [in Buechi.NecessityRF]
aut_inf_merging_correct [in Buechi.NecessityRF]
aut_exists_inf_merging_correct [in Buechi.NecessityRF]
aut_accepts_nfa_omega_iter [in Buechi.Buechi]
aut_accepts_image [in Buechi.Buechi]
aut1_incl_autU [in Buechi.Buechi]
AU_equiv_AC [in Buechi.NecessityRF]
AX_implies_RP [in Buechi.NecessityRF]

B

begin_pos_smonotone [in Buechi.AdditiveRamsey]
between_accepting_state_transforms_not_accepting [in Buechi.Buechi]
between_accepting_state_transforms_not_accepting' [in Buechi.Buechi]
between_accepting_state_intersect_is_accepting_state_aut_1 [in Buechi.Buechi]
bigAndCorrect [in Buechi.FullS1S]
bigEx2_correct [in Buechi.FullS1S]
bigOrCorrect [in Buechi.FullS1S]
bigpi_bigzip_inv [in Buechi.Sequences]
bigpi_correct [in Buechi.Sequences]
bigUpdate2_update [in Buechi.FullS1S]
bigUpdate2_unchanged [in Buechi.FullS1S]
bigzip_correct [in Buechi.Sequences]
bigzip_correct' [in Buechi.Sequences]
big_or_false [in Buechi.RamseyanFactorizations]
big_or_true [in Buechi.RamseyanFactorizations]
big_union_correct [in Buechi.Buechi]
boolOption_enum_ok [in FinTypes.FinTypes]
bool_enum_ok [in FinTypes.FinTypes]
bot_correct [in Buechi.FullS1S]
bounded_pred [in Buechi.Utils]

C

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]
cc_nat_first_geq_exists_extensional [in Buechi.Utils]
cc_nat_first_geq_exists_extensional' [in Buechi.Utils]
cc_nat_first_geq_exists_eq [in Buechi.Utils]
cc_nat_first_geq_exists_all [in Buechi.Utils]
cc_nat_first_geq_exists_correct [in Buechi.Utils]
cc_nat_first_geq_exists_increasing [in Buechi.Utils]
cc_nat_first_geq_all [in Buechi.Utils]
cc_nat_first_geq_bounds [in Buechi.Utils]
cc_nat_first_geq_correct [in Buechi.Utils]
cc_nat_first_extensional [in Buechi.Utils]
cc_nat [in Buechi.Utils]
cc_nat_first [in Buechi.Utils]
choose_sym_correct [in Buechi.Buechi]
closed_prefix_map [in Buechi.Sequences]
closed_substr_prepend [in Buechi.Sequences]
closed_prefix_eq [in Buechi.Sequences]
closed_substr_nstr_drop [in Buechi.Sequences]
closed_substr_singleton [in Buechi.Sequences]
closed_substr_shift [in Buechi.Sequences]
closed_substr_step_last [in Buechi.Sequences]
closed_substr_step [in Buechi.Sequences]
closed_substr_begin [in Buechi.Sequences]
closed_substr_nth' [in Buechi.Sequences]
closed_substr_nth [in Buechi.Sequences]
closed_prefix_plus [in Buechi.Sequences]
closed_prefix_step [in Buechi.Sequences]
closed_prefix_nth [in Buechi.Sequences]
closed_substr_delta [in Buechi.Sequences]
closed_prefix_delta [in Buechi.Sequences]
closed_take_delta [in Buechi.Strings]
Closure [in FinTypes.FinTypes]
Closure_FCIter [in FinTypes.FinTypes]
combine_sum [in Buechi.RamseyanFactorizations]
combine_transforms_accepting_right [in Buechi.NFAs]
combine_transforms_accepting_left [in Buechi.NFAs]
combine_transforms [in Buechi.NFAs]
compatibility [in Buechi.Complement]
complement_exhaustive_up [in Buechi.Complement]
complement_exhaustive [in Buechi.Complement]
complement_kind_exhaustive [in Buechi.Complement]
complement_disjoint [in Buechi.Complement]
complement_aut_correct [in Buechi.MinimalS1S]
complete_induction [in Buechi.Utils]
concat_map_length [in FinTypes.FinTypes]
consAppend [in FinTypes.BasicDefinitions]
const_nth [in Buechi.Sequences]
cons_incll [in FinTypes.BasicDefinitions]
cons_admits_ramseyan_fac [in Buechi.RamseyanFactorizations]
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]
cut_map [in Buechi.Sequences]
cut_flatten_inv [in Buechi.Sequences]
cut_delta [in Buechi.Sequences]
cut_correct [in Buechi.Sequences]

D

decision_false [in Buechi.Utils]
decision_true [in Buechi.Utils]
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_min_sat_implies_dec_full_sat [in Buechi.FullS1S]
dec_singleton_sets [in Buechi.FullS1S]
dec_satisfaction_up [in Buechi.MinimalS1S]
dec_min_S1S_up_satisfaction [in Buechi.MinimalS1S]
dec_min_S1S_satisfaction [in Buechi.MinimalS1S]
dec_ex_transforms_accepting_informative [in Buechi.NFAs]
dec_ex_transforms_informative [in Buechi.NFAs]
dec_transforms_informative_bound [in Buechi.NFAs]
dec_up_in_lang [in Buechi.Buechi]
dec_buechi_empty_informative [in Buechi.Buechi]
dec_is_match [in Buechi.Buechi]
delta_length [in Buechi.Strings]
deMorgan_and' [in Buechi.Utils]
deMorgan_and [in Buechi.Utils]
deMorgan_or [in Buechi.Utils]
deMorgan_exists [in Buechi.Utils]
deMorgan_all_neg [in Buechi.Utils]
deMorgan_all [in Buechi.Utils]
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]
DM_not_exists [in FinTypes.External]
DM_or [in FinTypes.External]
DM_exists [in FinTypes.FinTypes]
DM_notAll [in FinTypes.FinTypes]
double_flatten_cut_inv [in Buechi.Sequences]
double_negation [in Buechi.Utils]
drop_map [in Buechi.Sequences]
drop_nth' [in Buechi.Sequences]
drop_nth [in Buechi.Sequences]
drop_plus [in Buechi.Sequences]
drop_tl [in Buechi.Sequences]
drop_step [in Buechi.Sequences]
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]
duplicates [in Buechi.Strings]

E

elementIn [in FinTypes.FinTypes]
el_correct [in Buechi.FullS1S]
emptySet_correct [in Buechi.FinSets]
Empty_set_enum_ok [in FinTypes.FinTypes]
empty_aut_correct [in Buechi.Buechi]
encodes_fact_tl_revert [in Buechi.AdditiveRamsey]
encodes_fact_tl_preserves_deltas [in Buechi.AdditiveRamsey]
encode_seq_nth [in Buechi.NecessityRF]
enum_ok_fromList [in FinTypes.FinTypes]
equalize_first_delta [in Buechi.UPSequences]
equalize_first_correct [in Buechi.UPSequences]
Equivalence_property_exists' [in FinTypes.FinTypes]
Equivalence_property_exists [in FinTypes.FinTypes]
Equivalence_property_all [in FinTypes.FinTypes]
equiv_apart_update' [in Buechi.FullS1S]
equiv_apart_update [in Buechi.FullS1S]
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]
exact_up_nfa_correct [in Buechi.Buechi]
extPow_length [in FinTypes.FinTypes]
ex_nfa_up [in Buechi.MinimalS1S]
ex_nfa_correct [in Buechi.MinimalS1S]
ex_transforms_accepting_cc [in Buechi.NFAs]
ex_transforms_cc [in Buechi.NFAs]
ex_aut_correct [in Buechi.NecessityRF]
ex1_correct [in Buechi.FullS1S]

F

factorisation_to_bseq_correct [in Buechi.AdditiveRamsey]
factorisation_to_bseq_infinite [in Buechi.AdditiveRamsey]
factorize_monotone [in Buechi.AdditiveRamsey]
factorize_proper [in Buechi.Sequences]
factorize_correct [in Buechi.Sequences]
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]
filter_partition [in Buechi.Strings]
filter_empty [in Buechi.Strings]
filter_unchanged [in Buechi.Strings]
finBigAndCorrect [in Buechi.FullS1S]
finBigEx2_correct [in Buechi.FullS1S]
finBigOrCorrect [in Buechi.FullS1S]
finBigUpdate2_changed [in Buechi.FullS1S]
finBigUpdate2_unchanged [in Buechi.FullS1S]
fInduction [in FinTypes.FinTypes]
finSet_rem_correct [in Buechi.FinSets]
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]
finUnion_correct [in Buechi.FinSets]
flatten_idempotent [in Buechi.AdditiveRamsey]
flatten_concat [in Buechi.Sequences]
flatten_cut_inv [in Buechi.Sequences]
flatten_fin_iter [in Buechi.Sequences]
flatten_rotate [in Buechi.Sequences]
flatten_factorize_inv [in Buechi.Sequences]
flatten_map [in Buechi.Sequences]
flatten_prepend [in Buechi.Sequences]
flatten_correct [in Buechi.Sequences]
flatten_step [in Buechi.Sequences]
flatten_valid [in Buechi.NFAs]
formula_nfa_equal [in Buechi.MinimalS1S]
formula_aut_correct [in Buechi.MinimalS1S]
fp_admissible [in FinTypes.FinTypes]
fp_card_admissible [in FinTypes.FinTypes]
fp_iter_trans [in FinTypes.FinTypes]
fp_trans [in FinTypes.FinTypes]
free_sings_correct [in Buechi.FullS1S]
free_sings'_correct [in Buechi.FullS1S]
fresh_correct [in Buechi.FullS1S]
full_s1s_up_sat_if_as_sat [in Buechi.FullS1S]
full_s1s_up_sat_obtain [in Buechi.FullS1S]
full_s1s_dec_up_satisfaction [in Buechi.FullS1S]
full_s1s_dec_up_satisfies [in Buechi.FullS1S]
full_s1s_dec [in Buechi.FullS1S]
full_s1s_satisfies_xm [in Buechi.FullS1S]
full_s1s_to_min_s1s_complete [in Buechi.FullS1S]
full_s1s_to_min_s1s_correct [in Buechi.FullS1S]
function_implies_seq [in Buechi.FullS1S]
FX_implies_RP [in Buechi.NecessityRF]
FX_implies_RP_sigma [in Buechi.NecessityRF]
f_merging [in Buechi.RamseyanPigeonholePrinciple]
f_g_merge [in Buechi.RamseyanPigeonholePrinciple]
f_smonotone [in Buechi.RamseyanPigeonholePrinciple]
f_g_merging [in Buechi.RamseyanPigeonholePrinciple]

G

gamma_is_homomorphisms [in Buechi.Complement]
getAt_correct [in FinTypes.FinTypes]
getImage_correct [in FinTypes.FinTypes]
getImage_length [in FinTypes.FinTypes]
getImage_in [in FinTypes.FinTypes]
guess_sum_rev [in Buechi.NecessityRF]
guess_sum [in Buechi.NecessityRF]
g_smonotone [in Buechi.RamseyanPigeonholePrinciple]

H

Hedberg [in FinTypes.BasicDefinitions]
HelpApply [in FinTypes.FinTypes]
homomorphism_cons [in Buechi.RegularLanguages]
homomorphism_singletons [in Buechi.RamseyanFactorizations]
H' [in Buechi.RamseyanPigeonholePrinciple]

I

iff_ex [in Buechi.Utils]
iff_all [in Buechi.Utils]
iff_impl_true [in Buechi.Utils]
iff_impl [in Buechi.Utils]
iff_neg [in Buechi.Utils]
imagesDupfree [in FinTypes.FinTypes]
imagesInnerLength [in FinTypes.FinTypes]
imagesNonempty [in FinTypes.FinTypes]
images_length [in FinTypes.FinTypes]
image_match [in Buechi.Buechi]
image_aut_correct [in Buechi.Buechi]
image_accepts_aut [in Buechi.Buechi]
impl_correct [in Buechi.FullS1S]
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 Buechi.MinimalS1S]
incl_language [in Buechi.MinimalS1S]
inConcatCons [in FinTypes.FinTypes]
InCount [in FinTypes.BasicDefinitions]
infinite_update [in Buechi.AdditiveRamsey]
infinite_bseq_to_factorisation_seg [in Buechi.AdditiveRamsey]
infinite_bseq_to_factorisation_correct [in Buechi.AdditiveRamsey]
inf_often_map [in Buechi.Sequences]
inf_often_flatten [in Buechi.Sequences]
inf_often_prepend [in Buechi.Sequences]
inf_often_cons [in Buechi.Sequences]
inf_merging_to_function [in Buechi.RamseyanPigeonholePrinciple]
inf_often_zip_offset [in Buechi.Buechi]
inImages [in FinTypes.FinTypes]
injectiveApply [in FinTypes.BasicDefinitions]
injective_dupfree [in FinTypes.FinTypes]
intermediate_sum_rev [in Buechi.NecessityRF]
intermediate_sum [in Buechi.NecessityRF]
intersection_incl_intersect [in Buechi.Buechi]
intersect_correct [in Buechi.FinSets]
intersect_match_second [in Buechi.Buechi]
intersect_transforms_accepting [in Buechi.Buechi]
intersect_transforms [in Buechi.Buechi]
intersect_correct [in Buechi.Buechi]
intersect_incl_aut2 [in Buechi.Buechi]
intersect_incl_aut1 [in Buechi.Buechi]
intersect_incl_aut1_acc [in Buechi.Buechi]
in_rem_iff [in FinTypes.External]
in_filter_iff [in FinTypes.External]
in_cons_neq [in FinTypes.External]
in_sing [in FinTypes.External]
in_undup [in FinTypes.FinTypes]
in_complement_nfa_iff [in Buechi.Complement]
in_nstr_of_leq_delta_iff [in Buechi.Strings]
in_nstr_of_delta_iff [in Buechi.Strings]
in_flatten_list_iff [in Buechi.Strings]
in_nstr [in Buechi.Strings]
in_buechi_implies_up [in Buechi.Buechi]
IP_implies_MP [in Buechi.RamseyanFactorizations]
irun_accepting [in Buechi.Buechi]
irun_step_accepting [in Buechi.Buechi]
irun_step_to_true [in Buechi.Buechi]
irun_initial [in Buechi.Buechi]
irun_valid [in Buechi.Buechi]
irun_same_states [in Buechi.Buechi]
irun_Snth [in Buechi.Buechi]
irun_0th [in Buechi.Buechi]
isSuccCorrect [in Buechi.FullS1S]
isSuccMemCorrect [in Buechi.FullS1S]
is_buechi_empty_correct [in Buechi.Buechi]
ItoM1_agree [in Buechi.FullS1S]
ItoM1_agree' [in Buechi.FullS1S]
ItoM2_agree [in Buechi.FullS1S]
ItoM2_agree' [in Buechi.FullS1S]

L

language_intersection_comm [in Buechi.Utils]
language_union_comm [in Buechi.Utils]
language_eq_symmetric [in Buechi.Utils]
language_eq_iff [in Buechi.Utils]
language_universal_iff [in Buechi.Utils]
language_empty_iff [in Buechi.Utils]
left_assoc_sum [in Buechi.RamseyanFactorizations]
left_assoc [in Buechi.RamseyanFactorizations]
lengthEq [in FinTypes.BasicDefinitions]
leq_correct [in Buechi.FullS1S]
less_nfa_correct [in Buechi.MinimalS1S]
less_language [in Buechi.MinimalS1S]
le_correct [in Buechi.FullS1S]
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 Buechi.Utils]
loop [in FinTypes.BasicDefinitions]
loop_admits_ramseyan_fac [in Buechi.RamseyanFactorizations]

M

main_all_equiv [in Buechi.NecessityRF]
makeSet_correct [in Buechi.FinSets]
makeSet_eq [in Buechi.FinSets]
map_nstr_prepend [in Buechi.Sequences]
map_nth [in Buechi.Sequences]
map_fst_omega [in Buechi.NecessityRF]
match_for_up [in Buechi.Buechi]
match_accepted [in Buechi.Buechi]
max_of_nat_string_correct' [in Buechi.RamseyanPigeonholePrinciple]
max_of_nat_string_correct [in Buechi.RamseyanPigeonholePrinciple]
max_le [in Buechi.Utils]
max_le_right [in Buechi.Utils]
max_le_left [in Buechi.Utils]
mem_factorisation_to_bseq [in Buechi.AdditiveRamsey]
merges_aut_correct [in Buechi.NecessityRF]
merge_extend [in Buechi.RamseyanPigeonholePrinciple]
merging_shift [in Buechi.RamseyanPigeonholePrinciple]
merging_finite_equiv_classes [in Buechi.RamseyanPigeonholePrinciple]
minsat_agree_as_up [in Buechi.MinimalS1S]
min_sat_xm_implies_full_sat_xm [in Buechi.FullS1S]
min_sat_iff_full_sat [in Buechi.FullS1S]
min_s1S_dec_obtain [in Buechi.MinimalS1S]
min_s1S_dec_satisfaction [in Buechi.MinimalS1S]
min_s1S_dec_satisfaction_informative [in Buechi.MinimalS1S]
min_s1s_satisfies_xm [in Buechi.MinimalS1S]
mul_yields_idempotent [in Buechi.FiniteSemigroups]
mul_mult [in Buechi.FiniteSemigroups]
mul_distr [in Buechi.FiniteSemigroups]
mul_comm [in Buechi.FiniteSemigroups]
mul_step [in Buechi.FiniteSemigroups]
mul_ge_0 [in Buechi.Utils]

N

negOr [in FinTypes.BasicDefinitions]
neg_correct [in Buechi.FullS1S]
neg_merging_sym [in Buechi.RamseyanPigeonholePrinciple]
new_run_accepting [in Buechi.Buechi]
new_run_initial [in Buechi.Buechi]
new_run_valid [in Buechi.Buechi]
nfa_omega_iter_correct [in Buechi.Buechi]
nfa_omega_iter_accepts_aut [in Buechi.Buechi]
NoneElement [in FinTypes.FinTypes]
nonempty_substr_is_closed [in Buechi.Sequences]
nonempty_prefix_is_closed [in Buechi.Sequences]
nonempty_iff_match [in Buechi.Buechi]
notInMapCons [in FinTypes.FinTypes]
notInZero [in FinTypes.BasicDefinitions]
notright_is_left [in Buechi.Buechi]
not_in_cons [in FinTypes.External]
not_merge_iff [in Buechi.NecessityRF]
nstr_to_bnstr_delta [in Buechi.AdditiveRamsey]
nstr_to_bnstr_false [in Buechi.AdditiveRamsey]
nstr_to_bnstr_true [in Buechi.AdditiveRamsey]
nstr_zip_append [in Buechi.UPSequences]
nstr_zip_nth [in Buechi.UPSequences]
nstr_zip_delta [in Buechi.UPSequences]
nstr_concat_assoc [in Buechi.Sequences]
nstr_concat_sing [in Buechi.Sequences]
nstr_concat_swap [in Buechi.Sequences]
nstr_concat'_step [in Buechi.Sequences]
nstr_os_nfa_correct [in Buechi.RegularLanguages]
nstr_finIter_length [in Buechi.Strings]
nstr_to_str_length [in Buechi.Strings]
nstr_to_str_to_nstr_idem [in Buechi.Strings]
nstr_nonempty [in Buechi.Strings]
nstr_concat_delta [in Buechi.Strings]
nstr_map_concat [in Buechi.Strings]
nstr_map_nth [in Buechi.Strings]
nstr_map_length [in Buechi.Strings]
nstr_map_delta [in Buechi.Strings]
nstr_size_induction [in Buechi.Strings]
nstr_concat_last [in Buechi.Strings]
nstr_finIter_delta [in Buechi.Strings]
nstr_concat'_nth_snd [in Buechi.Strings]
nstr_concat'_nth_fst [in Buechi.Strings]
nstr_drop_last_nth [in Buechi.Strings]
nstr_drop_last_delta [in Buechi.Strings]
nstr_concat'_delta [in Buechi.Strings]
nstr_last_delta [in Buechi.Strings]
nstr_to_str_eq [in Buechi.Strings]
nth_step [in Buechi.Sequences]
nth_first [in Buechi.Sequences]
nth_first_hd [in Buechi.Sequences]
nth_step_tl [in Buechi.Sequences]
NullMul [in FinTypes.BasicDefinitions]

O

obtain_match [in Buechi.Buechi]
occurences_all [in Buechi.Strings]
occurences_all_instances [in Buechi.Strings]
occurences_correct [in Buechi.Strings]
occurences_dupfree [in Buechi.Strings]
occurences_bound [in Buechi.Strings]
omega_iter_map [in Buechi.Sequences]
omega_iter_sing [in Buechi.Sequences]
omega_iter_iter [in Buechi.Sequences]
omega_iter_step [in Buechi.Sequences]
omega_iter_rotate [in Buechi.Sequences]
omega_iter_correct [in Buechi.Sequences]
one_color_nfa_correct' [in Buechi.RegularLanguages]
one_color_nfa_nonempty [in Buechi.RegularLanguages]
one_color_nfa_correct [in Buechi.RegularLanguages]
one_color_nfa_accepts_strings_of_color [in Buechi.RegularLanguages]
Option_Card [in FinTypes.FinTypes]
option_enum_ok [in FinTypes.FinTypes]
order_g_f [in Buechi.RamseyanPigeonholePrinciple]
or_correct [in Buechi.FullS1S]
os_nfa_correct [in Buechi.RegularLanguages]
os_nfa_only_accepts_x [in Buechi.RegularLanguages]
os_nfa_accepts_x [in Buechi.RegularLanguages]

P

pair_eq [in Buechi.Complement]
pair_eq3 [in Buechi.Buechi]
phi_merge_correct [in Buechi.NecessityRF]
phi_sum_eq_correct [in Buechi.NecessityRF]
phi_last_correct [in Buechi.NecessityRF]
phi_step_correct [in Buechi.NecessityRF]
phi_first_correct [in Buechi.NecessityRF]
phi_unique_correct [in Buechi.NecessityRF]
pick [in FinTypes.FinTypes]
pidgeonHole_bij [in FinTypes.FinTypes]
pidgeonHole_surj [in FinTypes.FinTypes]
pidgeonHole_inj [in FinTypes.FinTypes]
postfixes_contains_postfixes [in Buechi.RegularLanguages]
postfix_inversion [in Buechi.RegularLanguages]
power_extensional [in FinTypes.External]
power_nil [in FinTypes.External]
power_incl [in FinTypes.External]
pow_ge_zero [in Buechi.Utils]
pred_xm_RP [in Buechi.NecessityRF]
prefix_nth [in Buechi.Sequences]
prefix_length [in Buechi.Sequences]
prefix_admits_ramseyan_fac [in Buechi.RamseyanFactorizations]
prefix_of_function_length [in Buechi.FiniteSemigroups]
prefix_of_function_correct [in Buechi.FiniteSemigroups]
preimage_aut_correct [in Buechi.Buechi]
prepend_lang_split_position [in Buechi.Sequences]
prepend_nstr_first [in Buechi.Sequences]
prepend_nstr_assoc [in Buechi.Sequences]
prepend_nstr_nth_rest_sub [in Buechi.Sequences]
prepend_nth_rest' [in Buechi.Sequences]
prepend_nstr_nth_rest [in Buechi.Sequences]
prepend_nth_rest_sub [in Buechi.Sequences]
prepend_nth_rest [in Buechi.Sequences]
prepend_nstr_nth_first [in Buechi.Sequences]
prepend_nth_first [in Buechi.Sequences]
prepend_nfa_correct [in Buechi.Buechi]
prepend_aut_accepts_prepend_omega [in Buechi.Buechi]
prepend_aut_is_prepend_omega [in Buechi.Buechi]
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_nil [in FinTypes.BasicDefinitions]
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]
purify [in FinTypes.BasicDefinitions]

Q

quasi_run_implies_accepting [in Buechi.Buechi]

R

ramseyan_fac_combine [in Buechi.RamseyanFactorizations]
RamseyFac_iff_RamseyFac' [in Buechi.RamseyanFactorizations]
ramsey_fac_iff_homogenous [in Buechi.AdditiveRamsey]
ramsey_nfa_correct [in Buechi.NecessityRF]
ramsey_nfa_color_correct [in Buechi.NecessityRF]
RA_implies_RF [in Buechi.AdditiveRamsey]
remove_loops_nstr [in Buechi.NFAs]
remove_loops [in Buechi.NFAs]
remove_loop [in Buechi.NFAs]
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_injection_eq [in Buechi.MinimalS1S]
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_drop [in Buechi.Sequences]
revert_nstr_prepend [in Buechi.Sequences]
revert_prepend [in Buechi.Sequences]
RF_implies_FX [in Buechi.FullS1S]
RF_implies_RA [in Buechi.AdditiveRamsey]
RF_implies_RP [in Buechi.RamseyanPigeonholePrinciple]
RF_implies_IP [in Buechi.RamseyanFactorizations]
rho'_accepts [in Buechi.Buechi]
rho'_firsts [in Buechi.Buechi]
rightResult [in FinTypes.FinTypes]
RPc_holds [in Buechi.RamseyanPigeonholePrinciple]
RP_implies_RF [in Buechi.RamseyanPigeonholePrinciple]
rp_implies_inf_merging_pos [in Buechi.RamseyanPigeonholePrinciple]
RP_implies_IP [in Buechi.RamseyanPigeonholePrinciple]
RP_iff_RPc_pred [in Buechi.NecessityRF]

S

saccepting_ind_iff_snaccepting_ind [in Buechi.RegularLanguages]
safe_dclosed [in Buechi.Utils]
same_color_same_accepting_quasi [in Buechi.Complement]
same_color_transforms_accepting [in Buechi.Complement]
same_color_transforms [in Buechi.Complement]
satisfaction_sat_xm [in Buechi.MinimalS1S]
satisfies_fun_extensional_bi [in Buechi.FullS1S]
satisfies_fun_extensional [in Buechi.FullS1S]
satisfies_extensional [in Buechi.MinimalS1S]
sat_up_obtain [in Buechi.MinimalS1S]
sat_iff_aut_non_empty [in Buechi.MinimalS1S]
sat_xm_exists_not_merging [in Buechi.NecessityRF]
sat_xm_exists_index_inf_merging [in Buechi.NecessityRF]
sat_xm_exists_merging [in Buechi.NecessityRF]
sat_xm_nat_dec_exists [in Buechi.NecessityRF]
sat_xm_iff [in Buechi.Utils]
scons_correct [in Buechi.Sequences]
seq_implies_function [in Buechi.FullS1S]
seq_nth [in Buechi.Sequences]
seq_to_sets_nth [in Buechi.NecessityRF]
set_map_correct [in Buechi.FinSets]
set_eq' [in Buechi.FinSets]
set_eq [in Buechi.FinSets]
sigT_enum_ok [in FinTypes.FinTypes]
sigT_proj2_fun [in FinTypes.BasicDefinitions]
sigT_proj1_fun [in FinTypes.BasicDefinitions]
singletonSetCorrect1 [in Buechi.FullS1S]
singletonSetCorrect2 [in Buechi.FullS1S]
singleton_correct' [in Buechi.FinSets]
singleton_correct [in Buechi.FinSets]
singleton_is_singleton [in Buechi.FullS1S]
singleton_iff [in Buechi.FullS1S]
singleton_nfa_nstr_correct [in Buechi.RegularLanguages]
singleton_nfa_correct [in Buechi.RegularLanguages]
sing_correct [in Buechi.FullS1S]
sing_equiv [in Buechi.FullS1S]
size_induction [in FinTypes.External]
snlanguage_ind_iff_slanguage_ind [in Buechi.RegularLanguages]
SomeElement [in FinTypes.FinTypes]
split_string_eq [in Buechi.UPSequences]
split_transforms_accepting [in Buechi.NFAs]
split_transforms [in Buechi.NFAs]
states_do_not_mix [in Buechi.Buechi]
step_consistent_least_fp [in FinTypes.FinTypes]
step_trans_fp_incl [in FinTypes.FinTypes]
step_iter_consistent [in FinTypes.FinTypes]
Streicher_K [in FinTypes.BasicDefinitions]
strings_of_color_accepted_by_one_color_nfa [in Buechi.RegularLanguages]
string_fixed_length_cc' [in Buechi.Strings]
string_bounded_length_cc [in Buechi.Strings]
string_fixed_length_cc [in Buechi.Strings]
str_nth_nstr' [in Buechi.Strings]
str_nth_nstr [in Buechi.Strings]
str_to_nstr_idem' [in Buechi.Strings]
str_to_nstr_idem [in Buechi.Strings]
subset_eq [in Buechi.FinSets]
substr_flatten [in Buechi.AdditiveRamsey]
substr_nth [in Buechi.Sequences]
substr_length [in Buechi.Sequences]
substr'_split [in Buechi.Sequences]
substr'_prepend' [in Buechi.Sequences]
substr'_nth [in Buechi.Sequences]
substr'_delta [in Buechi.Sequences]
subType_enum_ok [in FinTypes.FinTypes]
subtype_extensionality [in FinTypes.BasicDefinitions]
suffixsums_aut_trans_correct [in Buechi.NecessityRF]
SumCard [in FinTypes.FinTypes]
sum_enum_ok [in FinTypes.FinTypes]
SUM_flatten [in Buechi.FiniteSemigroups]
SUM_is_homomorphism [in Buechi.FiniteSemigroups]
SUM_concat [in Buechi.FiniteSemigroups]
sum_aut_trans_correct [in Buechi.NecessityRF]
surjectiveApply [in FinTypes.BasicDefinitions]
surj_sub [in FinTypes.FinTypes]
switch_from_V_to_W [in Buechi.Buechi]
s_monotone_order_preserving [in Buechi.Utils]
s_monotone_order_preserving' [in Buechi.Utils]
s_monotone_bound [in Buechi.Utils]
s1s_DM_exist_neg [in Buechi.FullS1S]
s1s_DM_forall_neg [in Buechi.FullS1S]
s1s_DM_neg_and [in Buechi.FullS1S]
s1s_coincidence_bi [in Buechi.FullS1S]
s1s_coincidence' [in Buechi.FullS1S]
s1s_coincidence [in Buechi.FullS1S]

T

tau_transforms_zip [in Buechi.Buechi]
test_destruct_annotate [in Buechi.Sequences]
tl_preserves_encodes_fact [in Buechi.AdditiveRamsey]
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]
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]
toMinMSO_correct [in Buechi.FullS1S]
top_correct [in Buechi.FullS1S]
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]
totality [in Buechi.Complement]
totality_up [in Buechi.Complement]
to_min_s1s_complete [in Buechi.FullS1S]
to_min_s1s_correct [in Buechi.FullS1S]
transforms_accepting_run_cc [in Buechi.NFAs]
transforms_run_cc [in Buechi.NFAs]
transforms_accepting_equiv [in Buechi.NFAs]
transforms_iff_valid_path [in Buechi.NFAs]
transforms_equiv [in Buechi.NFAs]
transforms_accepting_iff [in Buechi.NFAs]
transforms_accepting_concat [in Buechi.NFAs]
transforms_concat [in Buechi.NFAs]
transforms_accepting_inv [in Buechi.NFAs]
transforms_inv [in Buechi.NFAs]
transforms_accepting_implies_transform [in Buechi.NFAs]
transforms_not_accepting_is_accepted [in Buechi.Buechi]
transforms_not_accepting_is_accepted' [in Buechi.Buechi]
transforms_accepting_image_aut_transforms_accepting_aut [in Buechi.Buechi]
transforms_image_aut_transforms_aut [in Buechi.Buechi]
transition_from_none [in Buechi.NecessityRF]
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_assoc [in Buechi.FinSets]
union_correct [in Buechi.FinSets]
union_correct [in Buechi.Buechi]
union_symmetric [in Buechi.Buechi]
union_symmetric_acc [in Buechi.Buechi]
unit_enum_ok [in FinTypes.FinTypes]
univ_aut_scorrect [in Buechi.RegularLanguages]
univ_aut_correct [in Buechi.Buechi]
update_equiv_apart' [in Buechi.FullS1S]
update_equiv_apart [in Buechi.FullS1S]
update_second_order [in Buechi.FullS1S]
update_first_order [in Buechi.FullS1S]
update_head_hd_correct [in Buechi.AdditiveRamsey]
update_true_mem [in Buechi.AdditiveRamsey]
update_false_mem [in Buechi.AdditiveRamsey]
up_zip_correct [in Buechi.UPSequences]
up_iter_loop_loop_length [in Buechi.UPSequences]
up_iter_loop_prefix [in Buechi.UPSequences]
up_iter_loop_correct [in Buechi.UPSequences]
up_eq_zip_correct [in Buechi.UPSequences]
up_prefix_correct [in Buechi.UPSequences]
up_map_correct [in Buechi.UPSequences]
up_nth_correct [in Buechi.UPSequences]
up_equiv [in Buechi.UPSequences]
up_cons_unfold [in Buechi.UPSequences]
up_drop_correct [in Buechi.UPSequences]
up_tl_correct [in Buechi.UPSequences]
up_hd_correct [in Buechi.UPSequences]
up_const_correct [in Buechi.UPSequences]
up_admits_ramseyan_fac [in Buechi.RamseyanFactorizations]

V

valid_path_remove [in Buechi.NFAs]
valid_run_transforms_everywhere [in Buechi.NFAs]
valid_run_is_path_everywhere [in Buechi.NFAs]
valid_run_cons [in Buechi.NFAs]
valid_run_drop [in Buechi.NFAs]
valid_run_tl [in Buechi.NFAs]
valid_run_extensional [in Buechi.NFAs]
valid_path_length [in Buechi.NFAs]
valid_path_nth [in Buechi.NFAs]
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 Buechi.Utils]
VW_part_of_complement_iff [in Buechi.Complement]
VW_aut_correct [in Buechi.Complement]

W

wrap_correct [in Buechi.Sequences]

Z

zip_map_fst [in Buechi.Sequences]
zip_drop [in Buechi.Sequences]
zip_nth [in Buechi.Sequences]

---

Constructor Index

A

accept_step [in Buechi.RegularLanguages]
accept_empty [in Buechi.RegularLanguages]
And [in Buechi.FullS1S]

D

DecPred [in FinTypes.External]
DecRel [in FinTypes.External]
dummy [in Buechi.Strings]
dupfreeC [in FinTypes.External]
dupfreeN [in FinTypes.External]

E

EqType [in FinTypes.External]

F

FEx [in Buechi.FullS1S]
FinType [in FinTypes.FinTypes]
FinTypeC [in FinTypes.FinTypes]

I

Inf [in Buechi.Sequences]

L

Le [in Buechi.FullS1S]

M

MAnd [in Buechi.MinimalS1S]
Mem [in Buechi.FullS1S]
MEx [in Buechi.MinimalS1S]
MIncl [in Buechi.MinimalS1S]
mkFinTypeCardAtLeast3 [in Buechi.FullS1S]
mknfa [in Buechi.NFAs]
mkSG [in Buechi.FiniteSemigroups]
mkUPSeq [in Buechi.UPSequences]
MLe [in Buechi.MinimalS1S]
MNeg [in Buechi.MinimalS1S]

N

naccept_step [in Buechi.RegularLanguages]
naccept_sing [in Buechi.RegularLanguages]
ncons [in Buechi.Strings]
Neg [in Buechi.FullS1S]

P

postfix_step [in Buechi.RegularLanguages]
postfix_base [in Buechi.RegularLanguages]

S

safeB [in Buechi.Utils]
safeS [in Buechi.Utils]
SEx [in Buechi.FullS1S]
sing [in Buechi.Strings]

T

trans_accepting_step [in Buechi.NFAs]
trans_accepting_base [in Buechi.NFAs]
trans_step [in Buechi.NFAs]
trans_base [in Buechi.NFAs]
trans_not_step [in Buechi.Buechi]
trans_not_base [in Buechi.Buechi]

V

valid_path_step [in Buechi.NFAs]
valid_path_base [in Buechi.NFAs]

W

wrp [in Buechi.Sequences]

---

Inductive Index

D

Dummy [in Buechi.Strings]
dupfree [in FinTypes.External]

F

Form [in Buechi.FullS1S]

I

inf_often [in Buechi.Sequences]

M

MinForm [in Buechi.MinimalS1S]

N

NStr [in Buechi.Strings]

P

postfix [in Buechi.RegularLanguages]

S

saccepting_ind [in Buechi.RegularLanguages]
safe [in Buechi.Utils]
snaccepting_ind [in Buechi.RegularLanguages]

T

transforms [in Buechi.NFAs]
transforms_accepting [in Buechi.NFAs]
transforms_not_accepting [in Buechi.Buechi]

V

valid_path [in Buechi.NFAs]

---

Projection Index

A

accepting_state_dec [in Buechi.NFAs]
accepting_state [in Buechi.NFAs]
add [in Buechi.FiniteSemigroups]
Assoc [in Buechi.FiniteSemigroups]
Aut [in Buechi.MinimalS1S]

C

class [in FinTypes.FinTypes]
complement_aut_exhaustive [in Buechi.MinimalS1S]
complement_aut_disjoint [in Buechi.MinimalS1S]
complement_aut [in Buechi.MinimalS1S]
const [in Buechi.Sequences]
const_correct [in Buechi.Sequences]

D

decide_rel [in FinTypes.External]
decide_pred [in FinTypes.External]
decide_eq [in FinTypes.External]
dec_emptiness [in Buechi.MinimalS1S]
dummy [in Buechi.Strings]
D1 [in Buechi.FullS1S]
D2 [in Buechi.FullS1S]
D3 [in Buechi.FullS1S]

E

elements [in Buechi.FiniteSemigroups]
enum [in FinTypes.FinTypes]
enum_ok [in FinTypes.FinTypes]
eqtype [in FinTypes.External]
ex_aut_correct [in Buechi.MinimalS1S]
ex_aut [in Buechi.MinimalS1S]

H

hd [in Buechi.Sequences]
hd_correct [in Buechi.Sequences]

I

incl_aut_correct [in Buechi.MinimalS1S]
incl_aut [in Buechi.MinimalS1S]
Inf [in Buechi.Sequences]
initial_state_dec [in Buechi.NFAs]
initial_state [in Buechi.NFAs]
intersect_aut_correct [in Buechi.MinimalS1S]
intersect_aut [in Buechi.MinimalS1S]

L

lang [in Buechi.MinimalS1S]
less_aut_correct [in Buechi.MinimalS1S]
less_aut [in Buechi.MinimalS1S]

M

map [in Buechi.Sequences]
map_correct [in Buechi.Sequences]

P

predicate [in FinTypes.External]

R

relation [in FinTypes.External]

S

scons [in Buechi.Sequences]
Seq [in Buechi.Sequences]
state [in Buechi.NFAs]

T

tl [in Buechi.Sequences]
tl_correct [in Buechi.Sequences]
transition [in Buechi.NFAs]
transition_dec [in Buechi.NFAs]
type [in FinTypes.FinTypes]

U

unwrp [in Buechi.Sequences]
up_loop [in Buechi.UPSequences]
up_prefix [in Buechi.UPSequences]

V

V [in Buechi.FullS1S]

X

x1 [in Buechi.FullS1S]
x2 [in Buechi.FullS1S]
x3 [in Buechi.FullS1S]

Z

zip [in Buechi.Sequences]
zip_correct [in Buechi.Sequences]

---

Section Index

A

ACIffRF [in Buechi.NecessityRF]
ACIffRF.RamseyNFA [in Buechi.NecessityRF]
AdditiveRamsey [in Buechi.AdditiveRamsey]
AXImpliesRP [in Buechi.NecessityRF]
AXImpliesRP.AutAll [in Buechi.NecessityRF]
AXImpliesRP.ExAut [in Buechi.NecessityRF]
AXImpliesRP.SatXM_RP.MergesAut [in Buechi.NecessityRF]
AXImpliesRP.SatXM_RP [in Buechi.NecessityRF]
AXImpliesRP.SuffixSumsAut [in Buechi.NecessityRF]
AXImpliesRP.SumAut [in Buechi.NecessityRF]

B

BaseSeqOperations [in Buechi.Sequences]
Buechi [in Buechi.Buechi]
Buechi.BuechiAutomaton [in Buechi.Buechi]
Buechi.ImageNFA [in Buechi.Buechi]
Buechi.Intersection [in Buechi.Buechi]
Buechi.Intersection.IRun [in Buechi.Buechi]
Buechi.Match [in Buechi.Buechi]
Buechi.NFAOmegaIteration [in Buechi.Buechi]
Buechi.PreImageNFA [in Buechi.Buechi]
Buechi.PrependNFA [in Buechi.Buechi]
Buechi.QuasiRun [in Buechi.Buechi]
Buechi.QuasiRun.QuasiRunImpliesAccepting [in Buechi.Buechi]
Buechi.SimpleAutomata [in Buechi.Buechi]
Buechi.Union [in Buechi.Buechi]
Buechi.Union.Def [in Buechi.Buechi]

C

Cardinality [in FinTypes.External]
ClassicalReasoning [in Buechi.FullS1S]
Complement [in Buechi.Complement]

D

DropTake [in Buechi.Strings]
Dupfree [in FinTypes.External]
DupFreeDis [in FinTypes.External]
DuplicateInString [in Buechi.Strings]

E

Equi [in FinTypes.External]

F

FactorizationsAsStrictlyMonotoneFunctions [in Buechi.AdditiveRamsey]
FactorizationToBooleanSequence [in Buechi.AdditiveRamsey]
FilterLemmas [in FinTypes.External]
FilterLemmas [in Buechi.Strings]
FilterLemmas_pq [in FinTypes.External]
FiniteClosureIteration [in FinTypes.FinTypes]
FiniteSemigroup [in Buechi.FiniteSemigroups]
FiniteSets [in Buechi.FinSets]
First [in Buechi.Utils]
FirstGeq [in Buechi.Utils]
FirstGeq.FirstGeq [in Buechi.Utils]
FirstGeq.FirstGeqExists [in Buechi.Utils]
Fixedpoints [in FinTypes.FinTypes]
FlattenList [in Buechi.Strings]
FullS1S [in Buechi.FullS1S]
FullS1S.Coincidence [in Buechi.FullS1S]
FullS1S.ConvertInterpretations [in Buechi.FullS1S]
FullS1S.ReduceFullS1S_to_MinS1S [in Buechi.FullS1S]
FXImpliesRP [in Buechi.NecessityRF]

I

Inclusion [in FinTypes.External]
IndexAccess [in Buechi.Strings]

L

LanguageLemmata [in Buechi.Utils]
Languages [in Buechi.Utils]

M

Membership [in FinTypes.External]
MinS1S [in Buechi.MinimalS1S]
MinS1SToBuechi [in Buechi.MinimalS1S]
MoreConnectives1 [in Buechi.FullS1S]
MoreConnectives2 [in Buechi.FullS1S]
MoreSequences [in Buechi.Sequences]
MoreSequences.Annotate [in Buechi.Sequences]
MoreSequences.Factorize [in Buechi.Sequences]
MoreSequences.InfOften [in Buechi.Sequences]
MoreSequences.Languages [in Buechi.Sequences]
MoreSequences.OmegaIteration [in Buechi.Sequences]

N

NonEmptyStrings [in Buechi.Strings]
NStrBoundedDelta [in Buechi.Strings]
NStrBoundedDelta.DecAndChoice [in Buechi.Strings]
NStrBoundedDelta.DecAndChoice' [in Buechi.Strings]
NStrFlatten [in Buechi.Strings]
NStrMap [in Buechi.Strings]

O

OneColorNFA [in Buechi.RegularLanguages]
OneStringNFA [in Buechi.RegularLanguages]

P

PowerRep [in FinTypes.External]

R

RamseyanFactorizations [in Buechi.RamseyanFactorizations]
RamseyanFactorizations.DefinitionAndBasics [in Buechi.RamseyanFactorizations]
RamseyanPigeonholePrinciple [in Buechi.RamseyanPigeonholePrinciple]
RamseyanPigeonholePrinciple.Merging [in Buechi.RamseyanPigeonholePrinciple]
RegularLanguages [in Buechi.RegularLanguages]
Removal [in FinTypes.External]
ResultsFullS1S [in Buechi.FullS1S]
ResultsFullS1S.ASSemantics [in Buechi.FullS1S]
ResultsFullS1S.UPSemantics [in Buechi.FullS1S]
RF_impl_IP_impl_MP [in Buechi.RamseyanFactorizations]
RPIffRF [in Buechi.RamseyanPigeonholePrinciple]
RPIffRF.RPImpliesRF [in Buechi.RamseyanPigeonholePrinciple]

S

SeqInstances [in Buechi.UPSequences]
SeqInstances.BaseUP [in Buechi.UPSequences]
SeqInstances.NStrZip [in Buechi.UPSequences]
SeqInstances.UPMap [in Buechi.UPSequences]
SeqInstances.UPZip [in Buechi.UPSequences]
SeqInstances.ZipEqUP [in Buechi.UPSequences]
SeqInstances.ZipEqUP.UPEqualizePrefix [in Buechi.UPSequences]
Sequences [in Buechi.Sequences]
SingletonNFA [in Buechi.RegularLanguages]
StrictMonotonicity [in Buechi.Utils]
StrToNStr [in Buechi.Strings]

T

Test [in FinTypes.FinTypes]
TransformsRelations [in Buechi.NFAs]
TransformsRelations.Decidability [in Buechi.NFAs]
TransitionGraph [in Buechi.NFAs]

U

Undup [in FinTypes.External]

W

WithConstLemmas [in Buechi.Sequences]
WithZipMapLemmas [in Buechi.Sequences]
WithZipMapLemmas.BigZip [in Buechi.Sequences]

---

Instance Index

A

accepting_dec_public [in Buechi.NFAs]
accepting_for_proper [in Buechi.Buechi]
accepting_proper [in Buechi.Buechi]
accepts_proper [in Buechi.Buechi]
admits_ramseyan_factorization_proper [in Buechi.RamseyanFactorizations]
and_dec [in FinTypes.External]
app_equi_proper [in FinTypes.External]
app_incl_proper [in FinTypes.External]

B

bigpi_proper [in Buechi.Sequences]
bool_eq_dec [in FinTypes.External]
bounded_strict_forall [in Buechi.Utils]
bounded_exist [in Buechi.Utils]
bounded_forall [in Buechi.Utils]
BuechiAbstractAutomaton [in Buechi.MinimalS1S]

C

card_equi_proper [in FinTypes.External]
closed_substr_proper [in Buechi.Sequences]
closed_prefix_proper [in Buechi.Sequences]
cons_equi_proper [in FinTypes.External]
cons_incl_proper [in FinTypes.External]
cut_proper [in Buechi.Sequences]

D

decp_dec [in FinTypes.External]
decRel_dec [in FinTypes.External]
dec_kind_compatible [in Buechi.Complement]
dec_string_exists_fixed_length' [in Buechi.Strings]
dec_string_exists_bounded_length [in Buechi.Strings]
dec_string_exists_fixed_length [in Buechi.Strings]
dec_ex_transforms_accepting [in Buechi.NFAs]
dec_ex_transforms [in Buechi.NFAs]
dec_transforms_accepting [in Buechi.NFAs]
dec_transforms [in Buechi.NFAs]
dec_valid_path [in Buechi.NFAs]
dec_match_bool [in Buechi.Utils]
dec_destruct_list [in Buechi.Utils]
dec_option [in Buechi.Utils]
dec_sum [in Buechi.Utils]
dec_pair [in Buechi.Utils]
dec_mem_empty [in Buechi.Buechi]
dec_is_buechi_nonempty [in Buechi.Buechi]
dec_is_buechi_empty [in Buechi.Buechi]
dec_exists_match [in Buechi.Buechi]
drop_proper [in Buechi.Sequences]
DummyDummy [in Buechi.Strings]
DummyNat [in Buechi.Strings]
DummyNatFunc [in Buechi.Strings]
DummyNStr [in Buechi.Strings]
Dummy_nonempty [in Buechi.Strings]

E

ElemDummy [in Buechi.Strings]
Empty_set_eq_dec [in FinTypes.BasicDefinitions]
equiv_apart_proper [in Buechi.MinimalS1S]
equi_Equivalence [in FinTypes.External]
eq_dec_sigT [in FinTypes.BasicDefinitions]

F

False_dec [in FinTypes.External]
False_eq_dec [in FinTypes.BasicDefinitions]
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]
finType_exists_dec [in FinTypes.FinTypes]
finType_forall_dec [in FinTypes.FinTypes]
flatten_proper [in Buechi.Sequences]
fromListC [in FinTypes.FinTypes]

H

hd_proper [in Buechi.Sequences]

I

iff_dec [in FinTypes.External]
ImageProper [in Buechi.Sequences]
impl_dec [in FinTypes.External]
incl_equi_proper [in FinTypes.External]
incl_preorder [in FinTypes.External]
inf_often_flatten_tl [in Buechi.Sequences]
inf_often_proper [in Buechi.Sequences]
inf_often_prepend_instance [in Buechi.Sequences]
inf_often_cons_instance [in Buechi.Sequences]
inf_often_drop [in Buechi.Sequences]
inf_often_tl [in Buechi.Sequences]
initial_dec_public [in Buechi.NFAs]
in_equi_proper [in FinTypes.External]
in_incl_proper [in FinTypes.External]
is_singleton_proper [in Buechi.FullS1S]

L

language_complement_proper [in Buechi.Utils]
language_difference_proper [in Buechi.Utils]
language_intersection_proper [in Buechi.Utils]
language_union_proper [in Buechi.Utils]
language_incl [in Buechi.Utils]
language_eq_mem [in Buechi.Utils]
language_eq_equivalence [in Buechi.Utils]
list_exists_dec [in FinTypes.External]
list_forall_dec [in FinTypes.External]
list_in_dec [in FinTypes.External]
list_eq_dec [in FinTypes.External]

M

map_proper [in Buechi.Sequences]
memSetProper [in Buechi.FullS1S]
merging_proper [in Buechi.RamseyanPigeonholePrinciple]

N

nat_le_dec [in FinTypes.External]
nat_eq_dec [in FinTypes.External]
not_dec [in FinTypes.External]
nstr_dec_eq [in Buechi.Strings]
nth_proper [in Buechi.Sequences]

O

OmegaIterProper [in Buechi.Sequences]
option_eq_dec [in FinTypes.BasicDefinitions]
or_dec [in FinTypes.External]

P

prefix_proper [in Buechi.Sequences]
PreImageProper [in Buechi.Sequences]
PrependNProper [in Buechi.Sequences]
PrependProper [in Buechi.Sequences]
prepend_proper [in Buechi.Sequences]
prod_eq_dec [in FinTypes.BasicDefinitions]

S

satisfies_proper [in Buechi.MinimalS1S]
sat_xm_satis [in Buechi.NecessityRF]
sat_xm_proper [in Buechi.Utils]
sat_xm_from_dec [in Buechi.Utils]
sat_xm_not [in Buechi.Utils]
sat_xm_or [in Buechi.Utils]
sat_xm_and [in Buechi.Utils]
scons_proper [in Buechi.Sequences]
SeqDummy [in Buechi.Sequences]
SeqNStrDummy [in Buechi.Sequences]
Sequence [in Buechi.Sequences]
SequenceWithConst [in Buechi.Sequences]
SequenceWithZipMap [in Buechi.Sequences]
seq_equiv_equiv [in Buechi.Sequences]
set_mem_proper [in Buechi.MinimalS1S]
strict_bounded_exist [in Buechi.Utils]
subset_proper [in Buechi.FullS1S]
substr_proper [in Buechi.Sequences]
substr'_proper [in Buechi.Sequences]
subType_eq_dec [in FinTypes.BasicDefinitions]
sum_eq_dec [in FinTypes.BasicDefinitions]

T

tl_proper [in Buechi.Sequences]
transition_dec_public [in Buechi.NFAs]
True_dec [in FinTypes.External]
True_eq_dec [in FinTypes.BasicDefinitions]

U

unit_eq_dec [in FinTypes.BasicDefinitions]
UPBuechiAbstractAutomaton [in Buechi.MinimalS1S]
UPSequence [in Buechi.UPSequences]
UPWithConst [in Buechi.UPSequences]
UPWithZipMap [in Buechi.UPSequences]

V

valid_run_proper [in Buechi.NFAs]
vector_eq_dec [in FinTypes.FinTypes]
V_1 [in Buechi.NecessityRF]

Z

zip_proper [in Buechi.Sequences]

---

Abbreviation Index

B

B [in Buechi.FullS1S]

I

isleft [in Buechi.Buechi]
isright [in Buechi.Buechi]

N

NatSet [in Buechi.FullS1S]
NatSet [in Buechi.FullS1S]
NatSet [in Buechi.NecessityRF]

R

Run [in Buechi.Buechi]

S

Str [in Buechi.Strings]

T

toV1 [in Buechi.FullS1S]
toV2 [in Buechi.FullS1S]

---

Definition Index

A

AC [in Buechi.NecessityRF]
accepting [in Buechi.Buechi]
accepting_quasi_run [in Buechi.Buechi]
accepting_for [in Buechi.Buechi]
accepts [in Buechi.Buechi]
addGamma [in Buechi.Complement]
additive [in Buechi.AdditiveRamsey]
admissible [in FinTypes.FinTypes]
admits_idempotent_ramseyan_factorization [in Buechi.RamseyanFactorizations]
admits_ramseyan_factorization [in Buechi.RamseyanFactorizations]
all_sings [in Buechi.FullS1S]
all_aut [in Buechi.NecessityRF]
annotate [in Buechi.Sequences]
applyVect [in FinTypes.FinTypes]
associative [in Buechi.FiniteSemigroups]
AU [in Buechi.NecessityRF]
aut_all_sums_different [in Buechi.NecessityRF]
aut_inf_merging [in Buechi.NecessityRF]
AX [in Buechi.NecessityRF]

B

begin_pos [in Buechi.AdditiveRamsey]
bigAnd [in Buechi.FullS1S]
bigEx2 [in Buechi.FullS1S]
bigOr [in Buechi.FullS1S]
bigpi [in Buechi.Sequences]
bigUpdate2 [in Buechi.FullS1S]
bigUpdate2_correct [in Buechi.FullS1S]
bigzip [in Buechi.Sequences]
bigzip' [in Buechi.Sequences]
big_union [in Buechi.Buechi]
bijective [in FinTypes.BasicDefinitions]
bot [in Buechi.FullS1S]

C

card [in FinTypes.External]
card [in Buechi.FinSets]
Cardinality [in FinTypes.FinTypes]
Card_X_eq [in FinTypes.FinTypes]
card' [in Buechi.FinSets]
cc_j_k [in Buechi.RamseyanPigeonholePrinciple]
cc_nat_first_geq_exists [in Buechi.Utils]
cc_nat_first_geq [in Buechi.Utils]
choose_sym [in Buechi.Buechi]
clear_X [in Buechi.MinimalS1S]
closed_substr [in Buechi.Sequences]
closed_prefix [in Buechi.Sequences]
closed_take [in Buechi.Strings]
color_transition [in Buechi.RegularLanguages]
complement [in Buechi.Complement]
compute_run [in Buechi.Buechi]
count [in FinTypes.BasicDefinitions]
cut [in Buechi.Sequences]
cut_seq [in Buechi.Sequences]

D

dec [in FinTypes.External]
decision [in FinTypes.External]
delta [in Buechi.Strings]
disjoint [in FinTypes.External]

E

elem [in FinTypes.FinTypes]
elemToFinType [in Buechi.Sequences]
emptySet [in Buechi.FinSets]
empty_language [in Buechi.Utils]
empty_aut [in Buechi.Buechi]
encodes_fact_tl [in Buechi.AdditiveRamsey]
encode_seq [in Buechi.NecessityRF]
equalize_first [in Buechi.UPSequences]
equi [in FinTypes.External]
equiv_apart [in Buechi.MinimalS1S]
exact_up_nfa [in Buechi.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]
ex_nfa [in Buechi.MinimalS1S]
ex_aut [in Buechi.NecessityRF]

F

f [in Buechi.RamseyanPigeonholePrinciple]
factorisation_to_bseq [in Buechi.AdditiveRamsey]
factorize [in Buechi.Sequences]
FAll [in Buechi.FullS1S]
FCIter [in FinTypes.FinTypes]
FCStep [in FinTypes.FinTypes]
filter [in FinTypes.External]
finBigAnd [in Buechi.FullS1S]
finBigEx2 [in Buechi.FullS1S]
finBigOr [in Buechi.FullS1S]
finBigUpdate2 [in Buechi.FullS1S]
finSet [in Buechi.FinSets]
finSet_rem [in Buechi.FinSets]
finType_BoolUnit [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]
finUnion [in Buechi.FinSets]
first [in Buechi.Utils]
flatten [in Buechi.Sequences]
flatten_list [in Buechi.Strings]
formula_aut [in Buechi.MinimalS1S]
fp [in FinTypes.FinTypes]
free_sings [in Buechi.FullS1S]
free_sings' [in Buechi.FullS1S]
free_svars [in Buechi.FullS1S]
free_fvars [in Buechi.FullS1S]
fresh [in Buechi.FullS1S]
fun_encodes_factorization [in Buechi.AdditiveRamsey]
FX [in Buechi.FullS1S]

G

g [in Buechi.RamseyanPigeonholePrinciple]
gamma [in Buechi.Complement]
Gamma [in Buechi.Complement]
getAt [in FinTypes.FinTypes]
getImage [in FinTypes.FinTypes]
getPosition [in FinTypes.FinTypes]

H

has_some_kind [in Buechi.Complement]
has_kind [in Buechi.Complement]
homogenous [in Buechi.AdditiveRamsey]

I

idempotent [in Buechi.FiniteSemigroups]
Image [in Buechi.Sequences]
image [in FinTypes.FinTypes]
images [in FinTypes.FinTypes]
image_aut [in Buechi.Buechi]
image_transition [in Buechi.Buechi]
inclp [in FinTypes.External]
incl_nfa [in Buechi.MinimalS1S]
index [in FinTypes.FinTypes]
infinite [in Buechi.AdditiveRamsey]
infinite_bseq_to_factorisation [in Buechi.AdditiveRamsey]
initial [in Buechi.Buechi]
injective [in FinTypes.BasicDefinitions]
intersect [in Buechi.FinSets]
intersect [in Buechi.Buechi]
intersection_transition [in Buechi.Buechi]
intersection_accepting [in Buechi.Buechi]
intersection_initial [in Buechi.Buechi]
intersection_state [in Buechi.Buechi]
IP [in Buechi.RamseyanFactorizations]
irun [in Buechi.Buechi]
irun_step [in Buechi.Buechi]
IsSucc [in Buechi.FullS1S]
IsSuccMem [in Buechi.FullS1S]
is_singleton [in Buechi.FullS1S]
is_ramseyan_factorization [in Buechi.RamseyanFactorizations]
is_homomorphism [in Buechi.FiniteSemigroups]
is_buechi_empty [in Buechi.Buechi]
is_match [in Buechi.Buechi]
ItoM0 [in Buechi.FullS1S]
ItoM1 [in Buechi.FullS1S]
ItoM2 [in Buechi.FullS1S]

K

kind_compatible [in Buechi.Complement]

L

Language [in Buechi.Utils]
language_difference [in Buechi.Utils]
language_complement [in Buechi.Utils]
language_intersection [in Buechi.Utils]
language_union [in Buechi.Utils]
language_eq [in Buechi.Utils]
language_inclusion [in Buechi.Utils]
least_fp_containing [in FinTypes.FinTypes]
Leq [in Buechi.FullS1S]
less_nfa [in Buechi.MinimalS1S]

M

makeSet [in Buechi.FinSets]
max_of_nat_string [in Buechi.RamseyanPigeonholePrinciple]
mC [in FinTypes.FinTypes]
memSet [in Buechi.FullS1S]
merge [in Buechi.RamseyanPigeonholePrinciple]
merges_aut [in Buechi.NecessityRF]
merge_at [in Buechi.RamseyanPigeonholePrinciple]
mmC [in FinTypes.FinTypes]
MP [in Buechi.RamseyanFactorizations]
mul [in Buechi.FiniteSemigroups]

N

naligned [in Buechi.NFAs]
nfa_omega_iter [in Buechi.Buechi]
nlst_step [in Buechi.NFAs]
nonempty [in Buechi.Strings]
nstr_to_bnstr [in Buechi.AdditiveRamsey]
nstr_zip [in Buechi.UPSequences]
nstr_of_leq_delta [in Buechi.Strings]
nstr_of_delta [in Buechi.Strings]
nstr_drop [in Buechi.Strings]
nstr_flatten [in Buechi.Strings]
nstr_map [in Buechi.Strings]
nstr_finIter [in Buechi.Strings]
nstr_last [in Buechi.Strings]
nstr_drop_last [in Buechi.Strings]
nstr_concat' [in Buechi.Strings]
nstr_concat [in Buechi.Strings]
nstr_nth [in Buechi.Strings]
nstr_to_str [in Buechi.Strings]

O

occurences [in Buechi.Strings]
oiter_transition [in Buechi.Buechi]
OmegaIter [in Buechi.Sequences]
omega_iter [in Buechi.Sequences]
once [in Buechi.Sequences]
one_color_nfa [in Buechi.RegularLanguages]
Or [in Buechi.FullS1S]
os_nfa [in Buechi.RegularLanguages]

P

phi_merge [in Buechi.NecessityRF]
phi_sum_eq [in Buechi.NecessityRF]
phi_last [in Buechi.NecessityRF]
phi_step [in Buechi.NecessityRF]
phi_first [in Buechi.NecessityRF]
phi_unique [in Buechi.NecessityRF]
pickx [in FinTypes.FinTypes]
postfixes [in Buechi.RegularLanguages]
postfix_state [in Buechi.RegularLanguages]
power [in FinTypes.External]
prefix [in Buechi.Sequences]
prefix_of_function [in Buechi.FiniteSemigroups]
PreImage [in Buechi.Sequences]
preimage_aut [in Buechi.Buechi]
Prepend [in Buechi.Sequences]
prepend [in Buechi.Sequences]
PrependN [in Buechi.Sequences]
prepend_nfa [in Buechi.Buechi]
prepend_state_initial [in Buechi.Buechi]
prepend_state_accepting [in Buechi.Buechi]
prepend_transition [in Buechi.Buechi]
prodLists [in FinTypes.BasicDefinitions]
pure [in FinTypes.BasicDefinitions]
P1 [in Buechi.NecessityRF]
P2 [in Buechi.NecessityRF]
P3 [in Buechi.NecessityRF]

R

RA [in Buechi.AdditiveRamsey]
ramsey_nfa [in Buechi.NecessityRF]
ramsey_nfa_color [in Buechi.NecessityRF]
rem [in FinTypes.External]
rep [in FinTypes.External]
RF [in Buechi.RamseyanFactorizations]
RF' [in Buechi.RamseyanFactorizations]
rho' [in Buechi.Buechi]
RP [in Buechi.RamseyanPigeonholePrinciple]
RPc [in Buechi.RamseyanPigeonholePrinciple]
RPc_sigma [in Buechi.RamseyanPigeonholePrinciple]
RP_sigma [in Buechi.RamseyanPigeonholePrinciple]
Run [in Buechi.NFAs]

S

SAll [in Buechi.FullS1S]
sat [in Buechi.FullS1S]
sat [in Buechi.MinimalS1S]
satisfies [in Buechi.FullS1S]
satisfies [in Buechi.MinimalS1S]
satisfies_fun [in Buechi.FullS1S]
sat_xm [in Buechi.Utils]
seq_factorize [in Buechi.Sequences]
seq_flatten [in Buechi.Sequences]
seq_to_sets [in Buechi.NecessityRF]
seq_irun [in Buechi.Buechi]
set_map [in Buechi.FinSets]
set_mem [in Buechi.MinimalS1S]
Sing [in Buechi.FullS1S]
singleton [in Buechi.FinSets]
singletonSet [in Buechi.FullS1S]
singleton_lang [in Buechi.RegularLanguages]
singleton_nfa [in Buechi.RegularLanguages]
slanguage_ind [in Buechi.RegularLanguages]
snlanguage_ind [in Buechi.RegularLanguages]
step_consistent [in FinTypes.FinTypes]
str_nth [in Buechi.Strings]
str_to_nstr [in Buechi.Strings]
subset [in Buechi.FinSets]
subset [in Buechi.FullS1S]
substr [in Buechi.Sequences]
substr' [in Buechi.Sequences]
subtype [in FinTypes.BasicDefinitions]
success2 [in FinTypes.FinTypes]
success3 [in FinTypes.FinTypes]
suffixsums_aut [in Buechi.NecessityRF]
suffixsums_aut_trans [in Buechi.NecessityRF]
SUM [in Buechi.FiniteSemigroups]
sum_occurences [in Buechi.Strings]
sum_aut [in Buechi.NecessityRF]
sum_aut_trans [in Buechi.NecessityRF]
surjective [in FinTypes.BasicDefinitions]
swap_sum [in Buechi.Buechi]
s_monotone [in Buechi.Utils]
s1s_impl [in Buechi.FullS1S]

T

toeqType [in FinTypes.BasicDefinitions]
tofinType [in FinTypes.FinTypes]
toMinMSO [in Buechi.FullS1S]
toMinMSO' [in Buechi.FullS1S]
toOptionList [in FinTypes.BasicDefinitions]
top [in Buechi.FullS1S]
toright [in Buechi.Buechi]
toSigTList [in FinTypes.FinTypes]
toSubList [in FinTypes.FinTypes]
toSumList1 [in FinTypes.BasicDefinitions]
toSumList2 [in FinTypes.BasicDefinitions]

U

undup [in FinTypes.External]
unfold [in Buechi.UPSequences]
union [in Buechi.FinSets]
union [in Buechi.Buechi]
union_accepting [in Buechi.Buechi]
union_initial [in Buechi.Buechi]
union_transition [in Buechi.Buechi]
universal_language [in Buechi.Utils]
univ_aut [in Buechi.NFAs]
update_head [in Buechi.AdditiveRamsey]
up_zip [in Buechi.UPSequences]
up_iter_loop [in Buechi.UPSequences]
up_eq_zip [in Buechi.UPSequences]
up_map [in Buechi.UPSequences]
up_const [in Buechi.UPSequences]
up_cons [in Buechi.UPSequences]
up_tl [in Buechi.UPSequences]
up_hd [in Buechi.UPSequences]

V

valid_run [in Buechi.NFAs]
Var [in Buechi.FullS1S]
vector [in FinTypes.FinTypes]
vectorise [in FinTypes.FinTypes]
VW_aut [in Buechi.Complement]
V_2 [in Buechi.NecessityRF]

W

wrap [in Buechi.Sequences]

X

X [in Buechi.NecessityRF]

Y

Y [in Buechi.NecessityRF]

Z

zipFinTypes [in Buechi.Sequences]

---

Record Index

A

AbstractAutomata [in Buechi.MinimalS1S]
AbstractSequence [in Buechi.Sequences]

D

decPred [in FinTypes.External]
decRel [in FinTypes.External]
Dummy [in Buechi.Strings]

E

eqType [in FinTypes.External]

F

FiniteSemigroup [in Buechi.FiniteSemigroups]
finType [in FinTypes.FinTypes]
finTypeC [in FinTypes.FinTypes]
finTypeCardAtLeast3 [in Buechi.FullS1S]

I

inf_often [in Buechi.Sequences]

N

NFA [in Buechi.NFAs]

U

UPSeq [in Buechi.UPSequences]

W

WithConst [in Buechi.Sequences]
WithZipMap [in Buechi.Sequences]
WSeq [in Buechi.Sequences]

---

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

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

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

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

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

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

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

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

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

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

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

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

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

(16 entries)