| 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 | (393 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 | (6 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 | (51 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 | (8 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 | (171 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 | (6 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 | (16 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 | (1 entry) |
| 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 | (25 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 | (104 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 | (5 entries) |
Global Index
A
abl [definition, in abl]abl_pred0 [lemma, in abl_pred0]
abl_last [lemma, in abl_last]
abl_impl [lemma, in abl_impl]
abl_cat [lemma, in abl_cat]
abl_rcons [lemma, in abl_rcons]
abl0 [lemma, in abl0]
abl2s [lemma, in abl2s]
AllButLast [section, in AllButLast]
AllButLastDef [section, in AllButLastDef]
AllButLastDef.p [variable, in p]
AllButLastDef.X [variable, in X]
AllButLast.p [variable, in p]
AllButLast.q [variable, in q]
AllButLast.X [variable, in X]
all_abl_cat [lemma, in all_abl_cat]
all_abl [lemma, in all_abl]
all1s [lemma, in all1s]
Atom [constructor, in Atom]
atom [definition, in atom]
automata [library]
B
Basics [section, in Basics]Basics.char [variable, in char]
belast [definition, in belast]
belast_s1s [lemma, in belast_s1s]
belast_rcons [lemma, in belast_rcons]
big_plusP [lemma, in big_plusP]
big_plus_seqP [lemma, in big_plus_seqP]
bij_card [lemma, in bij_card]
C
can_iso_inv [lemma, in can_iso_inv]can_iso [lemma, in can_iso]
cardT_eq [lemma, in cardT_eq]
card_leq_inj [lemma, in card_leq_inj]
cat_nseq_eq [lemma, in cat_nseq_eq]
class [definition, in class]
class_eq [lemma, in class_eq]
coll [definition, in coll]
collapsed [definition, in collapsed]
collb [definition, in collb]
collb_trans [lemma, in collb_trans]
collb_sym [lemma, in collb_sym]
collb_refl [lemma, in collb_refl]
collb_step [lemma, in collb_step]
collP [lemma, in collP]
coll_iso [lemma, in coll_iso]
compl [definition, in compl]
Conc [constructor, in Conc]
conc [definition, in conc]
concP [lemma, in concP]
conc_inrP [lemma, in conc_inrP]
conc_inlP [lemma, in conc_inlP]
conc_eq [lemma, in conc_eq]
conc_cat [lemma, in conc_cat]
connected [definition, in connected]
connectedb [definition, in connectedb]
connectedP [lemma, in connectedP]
countL [lemma, in countL]
countR [lemma, in countR]
count_nseq [lemma, in count_nseq]
cr [definition, in cr]
crK [lemma, in crK]
D
delta [definition, in delta]delta_iso_inv [lemma, in delta_iso_inv]
delta_cat [lemma, in delta_cat]
delta_accept [lemma, in delta_accept]
delta_s_right_congruent [lemma, in delta_s_right_congruent]
delta_s_finPar [definition, in delta_s_finPar]
delta_cons [lemma, in delta_cons]
delta_iso [lemma, in delta_iso]
delta_s_refines [lemma, in delta_s_refines]
delta_s [definition, in delta_s]
dfa [record, in dfa]
dfac_to_myhill [definition, in dfac_to_myhill]
dfa_lang_emptyP [lemma, in dfa_lang_emptyP]
dfa_prune_correct [lemma, in dfa_prune_correct]
dfa_preimP [lemma, in dfa_preimP]
dfa_void_correct [lemma, in dfa_void_correct]
dfa_op [definition, in dfa_op]
dfa_equiv_correct [lemma, in dfa_equiv_correct]
dfa_sym_diff [definition, in dfa_sym_diff]
dfa_preim [definition, in dfa_preim]
dfa_run_take [lemma, in dfa_run_take]
dfa_to_nfa_correct [lemma, in dfa_to_nfa_correct]
dfa_trans1 [lemma, in dfa_trans1]
dfa_run [definition, in dfa_run]
dfa_L [lemma, in dfa_L]
dfa_to_re_correct [lemma, in dfa_to_re_correct]
dfa_iso_size [lemma, in dfa_iso_size]
dfa_to_re [definition, in dfa_to_re]
dfa_state [projection, in dfa_state]
dfa_compl_correct [lemma, in dfa_compl_correct]
dfa_equiv [definition, in dfa_equiv]
dfa_accept_cons [lemma, in dfa_accept_cons]
dfa_run_cat [lemma, in dfa_run_cat]
dfa_to_myhill_size [lemma, in dfa_to_myhill_size]
dfa_lang_empty [definition, in dfa_lang_empty]
dfa_to_nerode [definition, in dfa_to_nerode]
dfa_iso [definition, in dfa_iso]
dfa_op_correct [lemma, in dfa_op_correct]
dfa_lang [definition, in dfa_lang]
dfa_eps_correct [lemma, in dfa_eps_correct]
dfa_eps [definition, in dfa_eps]
dfa_prune_size [lemma, in dfa_prune_size]
dfa_preim_aux [lemma, in dfa_preim_aux]
dfa_compl [definition, in dfa_compl]
dfa_prune [definition, in dfa_prune]
dfa_trans_some [definition, in dfa_trans_some]
dfa_s [projection, in dfa_s]
dfa_fin [projection, in dfa_fin]
dfa_void [definition, in dfa_void]
dfa_trans [projection, in dfa_trans]
dfa_prune_connectedb_aux [lemma, in dfa_prune_connectedb_aux]
dfa_to_nfa [definition, in dfa_to_nfa]
dfa_accept [definition, in dfa_accept]
dfa_prune_connected [lemma, in dfa_prune_connected]
dfa_to_myhill [definition, in dfa_to_myhill]
dfa_to_re [library]
dist [definition, in dist]
distP [lemma, in distP]
distS [definition, in distS]
distSP [lemma, in distSP]
distS_mono [lemma, in distS_mono]
dist0 [definition, in dist0]
dlang [definition, in dlang]
E
edges [definition, in edges]edgesP [definition, in edgesP]
eps [definition, in eps]
Eps [constructor, in Eps]
eq_regexp_dec [lemma, in eq_regexp_dec]
F
FA [section, in FA]FA.char [variable, in char]
FA.Connected [section, in Connected]
FA.Connected.A [variable, in A]
FA.DFAOps [section, in DFAOps]
FA.DFAOps.A1 [variable, in A1]
FA.DFAOps.A2 [variable, in A2]
FA.DFAOps.op [variable, in op]
FA.DFA_Acceptance [section, in DFA_Acceptance]
FA.DFA_Acceptance.A [variable, in A]
FA.Embed [section, in Embed]
FA.Embed.A [variable, in A]
FA.Equivalence [section, in Equivalence]
FA.Isomopism [section, in Isomopism]
FA.Isomopism.A [variable, in A]
FA.Isomopism.A_conn [variable, in A_conn]
FA.Isomopism.A_coll [variable, in A_coll]
FA.Isomopism.B [variable, in B]
FA.Isomopism.B_coll [variable, in B_coll]
FA.Isomopism.B_conn [variable, in B_conn]
FA.Isomopism.L_AB [variable, in L_AB]
FA.Minimize [section, in Minimize]
FA.Minimize.A [variable, in A]
FA.NFAOps [section, in NFAOps]
FA.PowersetConstruction [section, in PowersetConstruction]
FA.PowersetConstruction.A [variable, in A]
FA.Reachability [section, in Reachability]
FA.Reachability.A [variable, in A]
finPar [record, in finPar]
finpar_fun [projection, in finpar_fun]
finpar_classes [projection, in finpar_classes]
finpar_surj [projection, in finpar_surj]
fin_app_pred [definition, in fin_app_pred]
FixPoint [section, in FixPoint]
FixPoint.F [variable, in F]
FixPoint.monoF [variable, in monoF]
FixPoint.T [variable, in T]
form_eqType [definition, in form_eqType]
fp_trans [definition, in fp_trans]
H
HomDef [section, in HomDef]HomDef.char [variable, in char]
HomDef.char' [variable, in char']
HomDef.h [variable, in h]
HomDef.h_hom [variable, in h_hom]
homomorphism [definition, in homomorphism]
Homomorphism [section, in Homomorphism]
homomorphism [library]
Homomorphism.char [variable, in char]
Homomorphism.char' [variable, in char']
Homomorphism.h [variable, in h]
Homomorphism.h_hom [variable, in h_hom]
h_seq [lemma, in h_seq]
h_flatten [lemma, in h_flatten]
h0 [lemma, in h0]
I
image [definition, in image]image_ext [lemma, in image_ext]
im_regular [lemma, in im_regular]
Inter [definition, in Inter]
Inter_correct [lemma, in Inter_correct]
iso [definition, in iso]
iso_inv [definition, in iso_inv]
iterFsub [lemma, in iterFsub]
iterFsubn [lemma, in iterFsubn]
iter_fix [lemma, in iter_fix]
L
L [definition, in L]Lab [definition, in Lab]
Lab_not_regular [lemma, in Lab_not_regular]
Lab_eq [lemma, in Lab_eq]
leq_eq [lemma, in leq_eq]
lfp [definition, in lfp]
lfpE [lemma, in lfpE]
lfp_ind [lemma, in lfp_ind]
LP [lemma, in LP]
L_split [lemma, in L_split]
L_nil [lemma, in L_nil]
L_R [lemma, in L_R]
L_star [lemma, in L_star]
L_catR [lemma, in L_catR]
L_monotone [lemma, in L_monotone]
L_rec [lemma, in L_rec]
L_cat [lemma, in L_cat]
L_catL [lemma, in L_catL]
M
mem_belast [lemma, in mem_belast]mem_R0 [lemma, in mem_R0]
minimal [definition, in minimal]
minimalP [lemma, in minimalP]
minimal_connected [lemma, in minimal_connected]
minimal_surj [lemma, in minimal_surj]
minimal_size_eq [lemma, in minimal_size_eq]
minimal_iso [lemma, in minimal_iso]
minimal_nerode [lemma, in minimal_nerode]
minimal_fin [lemma, in minimal_fin]
minimal_finPar [definition, in minimal_finPar]
minimal_idem [lemma, in minimal_idem]
minimize [definition, in minimize]
minimize_size [lemma, in minimize_size]
minimize_correct [lemma, in minimize_correct]
minimize_val [lemma, in minimize_val]
minimize_collapsed [lemma, in minimize_collapsed]
minimize_delta [lemma, in minimize_delta]
minimize_idem_size [lemma, in minimize_idem_size]
minimize_minimal [lemma, in minimize_minimal]
minimize_connected [lemma, in minimize_connected]
minstate_exp [lemma, in minstate_exp]
min_state [definition, in min_state]
misc [library]
mono [definition, in mono]
MyhillNerode [section, in MyhillNerode]
MyhillNerode.char [variable, in char]
MyhillNerode.mDFA_To_Nerode.MA [variable, in MA]
MyhillNerode.mDFA_To_Nerode.A [variable, in A]
MyhillNerode.mDFA_To_Nerode [section, in mDFA_To_Nerode]
myhillPar [record, in myhillPar]
myhill_lang_eq_proof [lemma, in myhill_lang_eq_proof]
myhill_to_dfa_correct [lemma, in myhill_to_dfa_correct]
myhill_lang_eq [definition, in myhill_lang_eq]
myhill_to_connected [lemma, in myhill_to_connected]
myhill_to_dfa [definition, in myhill_to_dfa]
myhill_congruent [projection, in myhill_congruent]
myhill_rel [projection, in myhill_rel]
myhill_nerode_spec [lemma, in myhill_nerode_spec]
myhill_refines [projection, in myhill_refines]
myhill_to_dfa_delta [lemma, in myhill_to_dfa_delta]
myhill_nerode [library]
N
Neg [definition, in Neg]Neg_correct [lemma, in Neg_correct]
nerode [definition, in nerode]
nerodeIN [lemma, in nerodeIN]
nerodeP [projection, in nerodeP]
nerodePar [record, in nerodePar]
nerode_par [projection, in nerode_par]
nerode_refines [lemma, in nerode_refines]
nerode_eq_proof [lemma, in nerode_eq_proof]
nerode_to_connected [lemma, in nerode_to_connected]
nerode_to_dfa [definition, in nerode_to_dfa]
nerode_right_congruent [lemma, in nerode_right_congruent]
nerode_to_myhill [definition, in nerode_to_myhill]
nerode_spec [definition, in nerode_spec]
nerode_to_dfa_correct [lemma, in nerode_to_dfa_correct]
nerode_eq [definition, in nerode_eq]
nfa [record, in nfa]
nfa_star_cat [lemma, in nfa_star_cat]
nfa_trans [projection, in nfa_trans]
nfa_star_correct [lemma, in nfa_star_correct]
nfa_star [definition, in nfa_star]
nfa_char_correct [lemma, in nfa_char_correct]
nfa_state [projection, in nfa_state]
nfa_to_dfa [definition, in nfa_to_dfa]
nfa_lang [definition, in nfa_lang]
nfa_to_dfa_aux2 [lemma, in nfa_to_dfa_aux2]
nfa_conc_correct [lemma, in nfa_conc_correct]
nfa_fin [projection, in nfa_fin]
nfa_accept [definition, in nfa_accept]
nfa_s [projection, in nfa_s]
nfa_starE [lemma, in nfa_starE]
nfa_to_dfa_correct [lemma, in nfa_to_dfa_correct]
nfa_starE_aux [lemma, in nfa_starE_aux]
nfa_char [definition, in nfa_char]
nfa_star_clone [lemma, in nfa_star_clone]
nfa_to_dfa_aux1 [lemma, in nfa_to_dfa_aux1]
nfa_conc [definition, in nfa_conc]
nfa_star_cont [lemma, in nfa_star_cont]
NonRegular [section, in NonRegular]
NonRegular.a [variable, in a]
NonRegular.b [variable, in b]
NonRegular.char [variable, in char]
NonRegular.Hab [variable, in Hab]
non_regular [library]
O
one_step_dist_mono [lemma, in one_step_dist_mono]one_step_dist [definition, in one_step_dist]
P
pigeon [lemma, in pigeon]Plus [constructor, in Plus]
plus [definition, in plus]
plusP [lemma, in plusP]
preimage [definition, in preimage]
preim_regular [lemma, in preim_regular]
prod [definition, in prod]
prune_eq_connected [lemma, in prune_eq_connected]
psym [lemma, in psym]
ptrans [lemma, in ptrans]
pumping [lemma, in pumping]
Pumping [section, in Pumping]
pumping [library]
Pumping.char [variable, in char]
pump_Lab [definition, in pump_Lab]
pump_dfa [lemma, in pump_dfa]
Q
Quot [section, in Quot]quot [definition, in quot]
Quot.e [variable, in e]
Quot.e_sym [variable, in e_sym]
Quot.e_refl [variable, in e_refl]
Quot.e_trans [variable, in e_trans]
Quot.T [variable, in T]
R
reachable [definition, in reachable]reachable_s [definition, in reachable_s]
reachable_trans [definition, in reachable_trans]
reachable_trans_proof [lemma, in reachable_trans_proof]
reachable_type [definition, in reachable_type]
refines [definition, in refines]
regexp [inductive, in regexp]
RegExp [section, in RegExp]
regexp [library]
regexp_eqMixin [definition, in regexp_eqMixin]
RegExp.char [variable, in char]
regular [definition, in regular]
regularE [lemma, in regularE]
regular_det [lemma, in regular_det]
regular_eq [lemma, in regular_eq]
regular_xm [lemma, in regular_xm]
ReLang [section, in ReLang]
ReLang.char [variable, in char]
rep [definition, in rep]
Repr [definition, in Repr]
repr [definition, in repr]
repr_rel [lemma, in repr_rel]
Repr_id [lemma, in Repr_id]
repr_idem [lemma, in repr_idem]
req_exp_predType [definition, in req_exp_predType]
residual [definition, in residual]
re_to_dfa [definition, in re_to_dfa]
re_to_dfa_correct [lemma, in re_to_dfa_correct]
re_image [definition, in re_image]
re_lang [definition, in re_lang]
re_equiv [definition, in re_equiv]
re_imageP [lemma, in re_imageP]
re_equiv_correct [lemma, in re_equiv_correct]
right_congruent [definition, in right_congruent]
run_cycle [lemma, in run_cycle]
run_size [lemma, in run_size]
run_word_split [lemma, in run_word_split]
run_split [lemma, in run_split]
R0 [definition, in R0]
S
set_op [definition, in set_op]set_pick_size [lemma, in set_pick_size]
set1mem [lemma, in set1mem]
size_induction [lemma, in size_induction]
Star [constructor, in Star]
star [definition, in star]
starI [lemma, in starI]
starP [lemma, in starP]
star_eq [lemma, in star_eq]
star_cat [lemma, in star_cat]
step_someP [lemma, in step_someP]
String [definition, in String]
StringE [lemma, in StringE]
surjective [definition, in surjective]
surjectiveE [lemma, in surjectiveE]
surj_card_bij [lemma, in surj_card_bij]
T
TransitiveClosure [section, in TransitiveClosure]TransitiveClosure.A [variable, in A]
TransitiveClosure.char [variable, in char]
L^ _ [notation, in ::'L^'_x]
R^ _ [notation, in ::'R^'_x]
\sigma_( _ <- _ ) _ [notation, in ::'\sigma_('_x_'<-'_x_')'_x]
\sigma_( _ | _ ) _ [notation, in ::'\sigma_('_x_'|'_x_')'_x]
U
uniqFE [lemma, in uniqFE]V
void [definition, in void]Void [constructor, in Void]
W
word [definition, in word]word [definition, in word]
word [definition, in word]
word_eqType [definition, in word_eqType]
other
Eps [notation, in ::'Eps']Void [notation, in ::'Void']
Notation Index
T
L^ _ [in ::'L^'_x]R^ _ [in ::'R^'_x]
\sigma_( _ <- _ ) _ [in ::'\sigma_('_x_'<-'_x_')'_x]
\sigma_( _ | _ ) _ [in ::'\sigma_('_x_'|'_x_')'_x]
other
Eps [in ::'Eps']Void [in ::'Void']
Variable Index
A
AllButLastDef.p [in p]AllButLastDef.X [in X]
AllButLast.p [in p]
AllButLast.q [in q]
AllButLast.X [in X]
B
Basics.char [in char]F
FA.char [in char]FA.Connected.A [in A]
FA.DFAOps.A1 [in A1]
FA.DFAOps.A2 [in A2]
FA.DFAOps.op [in op]
FA.DFA_Acceptance.A [in A]
FA.Embed.A [in A]
FA.Isomopism.A [in A]
FA.Isomopism.A_conn [in A_conn]
FA.Isomopism.A_coll [in A_coll]
FA.Isomopism.B [in B]
FA.Isomopism.B_coll [in B_coll]
FA.Isomopism.B_conn [in B_conn]
FA.Isomopism.L_AB [in L_AB]
FA.Minimize.A [in A]
FA.PowersetConstruction.A [in A]
FA.Reachability.A [in A]
FixPoint.F [in F]
FixPoint.monoF [in monoF]
FixPoint.T [in T]
H
HomDef.char [in char]HomDef.char' [in char']
HomDef.h [in h]
HomDef.h_hom [in h_hom]
Homomorphism.char [in char]
Homomorphism.char' [in char']
Homomorphism.h [in h]
Homomorphism.h_hom [in h_hom]
M
MyhillNerode.char [in char]MyhillNerode.mDFA_To_Nerode.MA [in MA]
MyhillNerode.mDFA_To_Nerode.A [in A]
N
NonRegular.a [in a]NonRegular.b [in b]
NonRegular.char [in char]
NonRegular.Hab [in Hab]
P
Pumping.char [in char]Q
Quot.e [in e]Quot.e_sym [in e_sym]
Quot.e_refl [in e_refl]
Quot.e_trans [in e_trans]
Quot.T [in T]
R
RegExp.char [in char]ReLang.char [in char]
T
TransitiveClosure.A [in A]TransitiveClosure.char [in char]
Library Index
A
automataD
dfa_to_reH
homomorphismM
miscmyhill_nerode
N
non_regularP
pumpingR
regexpLemma Index
A
abl_pred0 [in abl_pred0]abl_last [in abl_last]
abl_impl [in abl_impl]
abl_cat [in abl_cat]
abl_rcons [in abl_rcons]
abl0 [in abl0]
abl2s [in abl2s]
all_abl_cat [in all_abl_cat]
all_abl [in all_abl]
all1s [in all1s]
B
belast_s1s [in belast_s1s]belast_rcons [in belast_rcons]
big_plusP [in big_plusP]
big_plus_seqP [in big_plus_seqP]
bij_card [in bij_card]
C
can_iso_inv [in can_iso_inv]can_iso [in can_iso]
cardT_eq [in cardT_eq]
card_leq_inj [in card_leq_inj]
cat_nseq_eq [in cat_nseq_eq]
class_eq [in class_eq]
collb_trans [in collb_trans]
collb_sym [in collb_sym]
collb_refl [in collb_refl]
collb_step [in collb_step]
collP [in collP]
coll_iso [in coll_iso]
concP [in concP]
conc_inrP [in conc_inrP]
conc_inlP [in conc_inlP]
conc_eq [in conc_eq]
conc_cat [in conc_cat]
connectedP [in connectedP]
countL [in countL]
countR [in countR]
count_nseq [in count_nseq]
crK [in crK]
D
delta_iso_inv [in delta_iso_inv]delta_cat [in delta_cat]
delta_accept [in delta_accept]
delta_s_right_congruent [in delta_s_right_congruent]
delta_cons [in delta_cons]
delta_iso [in delta_iso]
delta_s_refines [in delta_s_refines]
dfa_lang_emptyP [in dfa_lang_emptyP]
dfa_prune_correct [in dfa_prune_correct]
dfa_preimP [in dfa_preimP]
dfa_void_correct [in dfa_void_correct]
dfa_equiv_correct [in dfa_equiv_correct]
dfa_run_take [in dfa_run_take]
dfa_to_nfa_correct [in dfa_to_nfa_correct]
dfa_trans1 [in dfa_trans1]
dfa_L [in dfa_L]
dfa_to_re_correct [in dfa_to_re_correct]
dfa_iso_size [in dfa_iso_size]
dfa_compl_correct [in dfa_compl_correct]
dfa_accept_cons [in dfa_accept_cons]
dfa_run_cat [in dfa_run_cat]
dfa_to_myhill_size [in dfa_to_myhill_size]
dfa_op_correct [in dfa_op_correct]
dfa_eps_correct [in dfa_eps_correct]
dfa_prune_size [in dfa_prune_size]
dfa_preim_aux [in dfa_preim_aux]
dfa_prune_connectedb_aux [in dfa_prune_connectedb_aux]
dfa_prune_connected [in dfa_prune_connected]
distP [in distP]
distSP [in distSP]
distS_mono [in distS_mono]
E
eq_regexp_dec [in eq_regexp_dec]H
h_seq [in h_seq]h_flatten [in h_flatten]
h0 [in h0]
I
image_ext [in image_ext]im_regular [in im_regular]
Inter_correct [in Inter_correct]
iterFsub [in iterFsub]
iterFsubn [in iterFsubn]
iter_fix [in iter_fix]
L
Lab_not_regular [in Lab_not_regular]Lab_eq [in Lab_eq]
leq_eq [in leq_eq]
lfpE [in lfpE]
lfp_ind [in lfp_ind]
LP [in LP]
L_split [in L_split]
L_nil [in L_nil]
L_R [in L_R]
L_star [in L_star]
L_catR [in L_catR]
L_monotone [in L_monotone]
L_rec [in L_rec]
L_cat [in L_cat]
L_catL [in L_catL]
M
mem_belast [in mem_belast]mem_R0 [in mem_R0]
minimalP [in minimalP]
minimal_connected [in minimal_connected]
minimal_surj [in minimal_surj]
minimal_size_eq [in minimal_size_eq]
minimal_iso [in minimal_iso]
minimal_nerode [in minimal_nerode]
minimal_fin [in minimal_fin]
minimal_idem [in minimal_idem]
minimize_size [in minimize_size]
minimize_correct [in minimize_correct]
minimize_val [in minimize_val]
minimize_collapsed [in minimize_collapsed]
minimize_delta [in minimize_delta]
minimize_idem_size [in minimize_idem_size]
minimize_minimal [in minimize_minimal]
minimize_connected [in minimize_connected]
minstate_exp [in minstate_exp]
myhill_lang_eq_proof [in myhill_lang_eq_proof]
myhill_to_dfa_correct [in myhill_to_dfa_correct]
myhill_to_connected [in myhill_to_connected]
myhill_nerode_spec [in myhill_nerode_spec]
myhill_to_dfa_delta [in myhill_to_dfa_delta]
N
Neg_correct [in Neg_correct]nerodeIN [in nerodeIN]
nerode_refines [in nerode_refines]
nerode_eq_proof [in nerode_eq_proof]
nerode_to_connected [in nerode_to_connected]
nerode_right_congruent [in nerode_right_congruent]
nerode_to_dfa_correct [in nerode_to_dfa_correct]
nfa_star_cat [in nfa_star_cat]
nfa_star_correct [in nfa_star_correct]
nfa_char_correct [in nfa_char_correct]
nfa_to_dfa_aux2 [in nfa_to_dfa_aux2]
nfa_conc_correct [in nfa_conc_correct]
nfa_starE [in nfa_starE]
nfa_to_dfa_correct [in nfa_to_dfa_correct]
nfa_starE_aux [in nfa_starE_aux]
nfa_star_clone [in nfa_star_clone]
nfa_to_dfa_aux1 [in nfa_to_dfa_aux1]
nfa_star_cont [in nfa_star_cont]
O
one_step_dist_mono [in one_step_dist_mono]P
pigeon [in pigeon]plusP [in plusP]
preim_regular [in preim_regular]
prune_eq_connected [in prune_eq_connected]
psym [in psym]
ptrans [in ptrans]
pumping [in pumping]
pump_dfa [in pump_dfa]
R
reachable_trans_proof [in reachable_trans_proof]regularE [in regularE]
regular_det [in regular_det]
regular_eq [in regular_eq]
regular_xm [in regular_xm]
repr_rel [in repr_rel]
Repr_id [in Repr_id]
repr_idem [in repr_idem]
re_to_dfa_correct [in re_to_dfa_correct]
re_imageP [in re_imageP]
re_equiv_correct [in re_equiv_correct]
run_cycle [in run_cycle]
run_size [in run_size]
run_word_split [in run_word_split]
run_split [in run_split]
S
set_pick_size [in set_pick_size]set1mem [in set1mem]
size_induction [in size_induction]
starI [in starI]
starP [in starP]
star_eq [in star_eq]
star_cat [in star_cat]
step_someP [in step_someP]
StringE [in StringE]
surjectiveE [in surjectiveE]
surj_card_bij [in surj_card_bij]
U
uniqFE [in uniqFE]Constructor Index
A
Atom [in Atom]C
Conc [in Conc]E
Eps [in Eps]P
Plus [in Plus]S
Star [in Star]V
Void [in Void]Projection Index
D
dfa_state [in dfa_state]dfa_s [in dfa_s]
dfa_fin [in dfa_fin]
dfa_trans [in dfa_trans]
F
finpar_fun [in finpar_fun]finpar_classes [in finpar_classes]
finpar_surj [in finpar_surj]
M
myhill_congruent [in myhill_congruent]myhill_rel [in myhill_rel]
myhill_refines [in myhill_refines]
N
nerodeP [in nerodeP]nerode_par [in nerode_par]
nfa_trans [in nfa_trans]
nfa_state [in nfa_state]
nfa_fin [in nfa_fin]
nfa_s [in nfa_s]
Inductive Index
R
regexp [in regexp]Section Index
A
AllButLast [in AllButLast]AllButLastDef [in AllButLastDef]
B
Basics [in Basics]F
FA [in FA]FA.Connected [in Connected]
FA.DFAOps [in DFAOps]
FA.DFA_Acceptance [in DFA_Acceptance]
FA.Embed [in Embed]
FA.Equivalence [in Equivalence]
FA.Isomopism [in Isomopism]
FA.Minimize [in Minimize]
FA.NFAOps [in NFAOps]
FA.PowersetConstruction [in PowersetConstruction]
FA.Reachability [in Reachability]
FixPoint [in FixPoint]
H
HomDef [in HomDef]Homomorphism [in Homomorphism]
M
MyhillNerode [in MyhillNerode]MyhillNerode.mDFA_To_Nerode [in mDFA_To_Nerode]
N
NonRegular [in NonRegular]P
Pumping [in Pumping]Q
Quot [in Quot]R
RegExp [in RegExp]ReLang [in ReLang]
T
TransitiveClosure [in TransitiveClosure]Definition Index
A
abl [in abl]atom [in atom]
B
belast [in belast]C
class [in class]coll [in coll]
collapsed [in collapsed]
collb [in collb]
compl [in compl]
conc [in conc]
connected [in connected]
connectedb [in connectedb]
cr [in cr]
D
delta [in delta]delta_s_finPar [in delta_s_finPar]
delta_s [in delta_s]
dfac_to_myhill [in dfac_to_myhill]
dfa_op [in dfa_op]
dfa_sym_diff [in dfa_sym_diff]
dfa_preim [in dfa_preim]
dfa_run [in dfa_run]
dfa_to_re [in dfa_to_re]
dfa_equiv [in dfa_equiv]
dfa_lang_empty [in dfa_lang_empty]
dfa_to_nerode [in dfa_to_nerode]
dfa_iso [in dfa_iso]
dfa_lang [in dfa_lang]
dfa_eps [in dfa_eps]
dfa_compl [in dfa_compl]
dfa_prune [in dfa_prune]
dfa_trans_some [in dfa_trans_some]
dfa_void [in dfa_void]
dfa_to_nfa [in dfa_to_nfa]
dfa_accept [in dfa_accept]
dfa_to_myhill [in dfa_to_myhill]
dist [in dist]
distS [in distS]
dist0 [in dist0]
dlang [in dlang]
E
edges [in edges]edgesP [in edgesP]
eps [in eps]
F
fin_app_pred [in fin_app_pred]form_eqType [in form_eqType]
fp_trans [in fp_trans]
H
homomorphism [in homomorphism]I
image [in image]Inter [in Inter]
iso [in iso]
iso_inv [in iso_inv]
L
L [in L]Lab [in Lab]
lfp [in lfp]
M
minimal [in minimal]minimal_finPar [in minimal_finPar]
minimize [in minimize]
min_state [in min_state]
mono [in mono]
myhill_lang_eq [in myhill_lang_eq]
myhill_to_dfa [in myhill_to_dfa]
N
Neg [in Neg]nerode [in nerode]
nerode_to_dfa [in nerode_to_dfa]
nerode_to_myhill [in nerode_to_myhill]
nerode_spec [in nerode_spec]
nerode_eq [in nerode_eq]
nfa_star [in nfa_star]
nfa_to_dfa [in nfa_to_dfa]
nfa_lang [in nfa_lang]
nfa_accept [in nfa_accept]
nfa_char [in nfa_char]
nfa_conc [in nfa_conc]
O
one_step_dist [in one_step_dist]P
plus [in plus]preimage [in preimage]
prod [in prod]
pump_Lab [in pump_Lab]
Q
quot [in quot]R
reachable [in reachable]reachable_s [in reachable_s]
reachable_trans [in reachable_trans]
reachable_type [in reachable_type]
refines [in refines]
regexp_eqMixin [in regexp_eqMixin]
regular [in regular]
rep [in rep]
Repr [in Repr]
repr [in repr]
req_exp_predType [in req_exp_predType]
residual [in residual]
re_to_dfa [in re_to_dfa]
re_image [in re_image]
re_lang [in re_lang]
re_equiv [in re_equiv]
right_congruent [in right_congruent]
R0 [in R0]
S
set_op [in set_op]star [in star]
String [in String]
surjective [in surjective]
V
void [in void]W
word [in word]word [in word]
word [in word]
word_eqType [in word_eqType]
Record Index
D
dfa [in dfa]F
finPar [in finPar]M
myhillPar [in myhillPar]N
nerodePar [in nerodePar]nfa [in nfa]
| 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 | (393 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 | (6 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 | (51 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 | (8 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 | (171 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 | (6 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 | (16 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 | (1 entry) |
| 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 | (25 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 | (104 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 | (5 entries) |
This page has been generated by coqdoc