| 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 | (758 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 | (17 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 | (103 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 | (12 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 | (324 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 | (24 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 | (7 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 | (30 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 | (42 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 | (9 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 | (181 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
Global Index
A
abstract_minimization [lemma, in RegLang.minimization]accE [definition, in RegLang.dfa]
accept [definition, in RegLang.wmso]
accept_cons [lemma, in RegLang.dfa]
accept_nil [lemma, in RegLang.dfa]
agree [definition, in RegLang.wmso]
agree_dc [lemma, in RegLang.wmso]
All [definition, in RegLang.wmso]
allseq_dec [lemma, in RegLang.dfa]
All1 [definition, in RegLang.wmso]
all1s [lemma, in RegLang.misc]
all1sT [lemma, in RegLang.misc]
And [definition, in RegLang.wmso]
atom [definition, in RegLang.languages]
Atom [constructor, in RegLang.regexp]
A_start_cat [lemma, in RegLang.dfa]
B
Basics [section, in RegLang.languages]Basics.char [variable, in RegLang.languages]
behead_cons [lemma, in RegLang.wmso]
bigmax_seq_sup [lemma, in RegLang.misc]
big_plus_size [lemma, in RegLang.regexp]
big_plusP [lemma, in RegLang.regexp]
big_plus_seqP [lemma, in RegLang.regexp]
bij_card [lemma, in RegLang.misc]
bound [definition, in RegLang.wmso]
bsimp [definition, in RegLang.vardi]
C
can_iso_inv [lemma, in RegLang.minimization]can_iso [lemma, in RegLang.minimization]
cards_lt1 [lemma, in RegLang.two_way]
cardT_eq [lemma, in RegLang.misc]
card_set [lemma, in RegLang.misc]
card_leq_inj [lemma, in RegLang.misc]
cat [definition, in RegLang.wmso]
cat_size [lemma, in RegLang.wmso]
cat_beyond [lemma, in RegLang.wmso]
cat_prefix [lemma, in RegLang.wmso]
cat_nseq_eq [lemma, in RegLang.dfa]
cf_lang_eq [definition, in RegLang.myhill_nerode]
cf_lang_eq_proof [lemma, in RegLang.myhill_nerode]
cf_refines [projection, in RegLang.myhill_nerode]
cf_congruent [projection, in RegLang.myhill_nerode]
cf_classifier [projection, in RegLang.myhill_nerode]
Clasifiers [section, in RegLang.myhill_nerode]
Clasifiers.char [variable, in RegLang.myhill_nerode]
Clasifiers.ClassifierToDFA [section, in RegLang.myhill_nerode]
Clasifiers.ClassifierToDFA.L [variable, in RegLang.myhill_nerode]
Clasifiers.ClassifierToDFA.M [variable, in RegLang.myhill_nerode]
Clasifiers.DFAtoClassifier [section, in RegLang.myhill_nerode]
Clasifiers.DFAtoClassifier.A [variable, in RegLang.myhill_nerode]
Clasifiers.mDFAtoMG [section, in RegLang.myhill_nerode]
Clasifiers.mDFAtoMG.A [variable, in RegLang.myhill_nerode]
Clasifiers.mDFAtoMG.MA [variable, in RegLang.myhill_nerode]
classes_of [abbreviation, in RegLang.myhill_nerode]
classifier [record, in RegLang.myhill_nerode]
Classifier [constructor, in RegLang.myhill_nerode]
classifier_to_dfa_connected [lemma, in RegLang.myhill_nerode]
classifier_to_dfa_correct [lemma, in RegLang.myhill_nerode]
classifier_to_dfa_delta [lemma, in RegLang.myhill_nerode]
classifier_to_dfa [definition, in RegLang.myhill_nerode]
classifier_for [record, in RegLang.myhill_nerode]
classifier_fun [projection, in RegLang.myhill_nerode]
classifier_classes [projection, in RegLang.myhill_nerode]
coincidence [lemma, in RegLang.wmso]
coll [definition, in RegLang.minimization]
collapse [definition, in RegLang.minimization]
collapsed [definition, in RegLang.minimization]
collapse_connected [lemma, in RegLang.minimization]
collapse_size [lemma, in RegLang.minimization]
collapse_correct [lemma, in RegLang.minimization]
collapse_collapsed [lemma, in RegLang.minimization]
collapse_fin [lemma, in RegLang.minimization]
collapse_delta [lemma, in RegLang.minimization]
collapse_state [definition, in RegLang.minimization]
collb [definition, in RegLang.minimization]
collb_step [lemma, in RegLang.minimization]
collb_trans [lemma, in RegLang.minimization]
collb_sym [lemma, in RegLang.minimization]
collb_refl [lemma, in RegLang.minimization]
collP [lemma, in RegLang.minimization]
coll_fun_RC [lemma, in RegLang.minimization]
coll_fun [definition, in RegLang.minimization]
coll_iso [lemma, in RegLang.minimization]
comp [definition, in RegLang.vardi]
compL [definition, in RegLang.vardi]
compl [definition, in RegLang.languages]
compR [definition, in RegLang.vardi]
conc [definition, in RegLang.languages]
Conc [constructor, in RegLang.regexp]
concP [lemma, in RegLang.languages]
conc_eq [lemma, in RegLang.languages]
conc_cat [lemma, in RegLang.languages]
connected [definition, in RegLang.minimization]
connectedb [definition, in RegLang.minimization]
connectedP [lemma, in RegLang.minimization]
connect_transfer [lemma, in RegLang.misc]
cons [definition, in RegLang.wmso]
contraN [lemma, in RegLang.shepherdson]
countL [lemma, in RegLang.dfa]
countR [lemma, in RegLang.dfa]
count_nseq [lemma, in RegLang.dfa]
cr [definition, in RegLang.misc]
crK [lemma, in RegLang.misc]
D
DecidableLanguages [section, in RegLang.languages]DecidableLanguages.char [variable, in RegLang.languages]
dec_eq [lemma, in RegLang.misc]
dec_iff [lemma, in RegLang.misc]
delta [definition, in RegLang.dfa]
delta_rep [lemma, in RegLang.dfa]
delta_rc [lemma, in RegLang.dfa]
delta_lang [lemma, in RegLang.dfa]
delta_s [definition, in RegLang.dfa]
delta_cat [lemma, in RegLang.dfa]
delta_cons [lemma, in RegLang.dfa]
delta_iso_inv [lemma, in RegLang.minimization]
delta_iso [lemma, in RegLang.minimization]
delta_s_refines [lemma, in RegLang.myhill_nerode]
delta_s_right_congruent [lemma, in RegLang.myhill_nerode]
detC [projection, in RegLang.two_way]
deterministic [record, in RegLang.two_way]
detL [projection, in RegLang.two_way]
detR [projection, in RegLang.two_way]
det_range [lemma, in RegLang.shepherdson]
dfa [record, in RegLang.dfa]
dfa [abbreviation, in RegLang.minimization]
dfa [library]
DFAofRE [section, in RegLang.regexp]
DFAofRE.char [variable, in RegLang.regexp]
DFAtoDFA2 [section, in RegLang.two_way]
DFAtoDFA2.A [variable, in RegLang.two_way]
DFAtoDFA2.char [variable, in RegLang.two_way]
DFAtoDFA2.n [variable, in RegLang.two_way]
DFAtoDFA2.w [variable, in RegLang.two_way]
dfa_quotP [lemma, in RegLang.dfa]
dfa_quot [definition, in RegLang.dfa]
dfa_preimP [lemma, in RegLang.dfa]
dfa_preim [definition, in RegLang.dfa]
dfa_incl_correct [lemma, in RegLang.dfa]
dfa_incl [definition, in RegLang.dfa]
dfa_equiv_correct [lemma, in RegLang.dfa]
dfa_equiv [definition, in RegLang.dfa]
dfa_emptyP [lemma, in RegLang.dfa]
dfa_empty [definition, in RegLang.dfa]
dfa_inhabP [lemma, in RegLang.dfa]
dfa_inhab [definition, in RegLang.dfa]
dfa_op_correct [lemma, in RegLang.dfa]
dfa_op [definition, in RegLang.dfa]
dfa_compl_correct [lemma, in RegLang.dfa]
dfa_compl [definition, in RegLang.dfa]
dfa_void_correct [lemma, in RegLang.dfa]
dfa_void [definition, in RegLang.dfa]
dfa_lang [definition, in RegLang.dfa]
dfa_accept [definition, in RegLang.dfa]
dfa_trans [projection, in RegLang.dfa]
dfa_fin [projection, in RegLang.dfa]
dfa_s [projection, in RegLang.dfa]
dfa_state [projection, in RegLang.dfa]
dfa_prune_size [lemma, in RegLang.minimization]
dfa_prune_connected [lemma, in RegLang.minimization]
dfa_prune_correct [lemma, in RegLang.minimization]
dfa_prune [definition, in RegLang.minimization]
dfa_iso_size [lemma, in RegLang.minimization]
dfa_iso [definition, in RegLang.minimization]
dfa_to_re_size [lemma, in RegLang.regexp]
dfa_to_re_correct [lemma, in RegLang.regexp]
dfa_to_re [definition, in RegLang.regexp]
dfa_L [lemma, in RegLang.regexp]
dfa_to_mg [definition, in RegLang.myhill_nerode]
dfa_to_cf_size [lemma, in RegLang.myhill_nerode]
dfa_to_cf [definition, in RegLang.myhill_nerode]
dfa_to_nfa_correct [lemma, in RegLang.nfa]
dfa_to_nfa [definition, in RegLang.nfa]
dfa0 [definition, in RegLang.dfa]
dfa0_correct [lemma, in RegLang.dfa]
dfa2 [record, in RegLang.two_way]
DFA2 [constructor, in RegLang.two_way]
DFA2 [section, in RegLang.two_way]
dfa2Pn [lemma, in RegLang.vardi]
DFA2toAFA [section, in RegLang.shepherdson]
DFA2toAFA.char [variable, in RegLang.shepherdson]
DFA2toAFA.M [variable, in RegLang.shepherdson]
dfa2_of_correct [lemma, in RegLang.two_way]
dfa2_of_dfa [definition, in RegLang.two_way]
dfa2_lang [definition, in RegLang.two_way]
dfa2_det [projection, in RegLang.two_way]
dfa2_to_dfa [lemma, in RegLang.shepherdson]
dfa2_to_myhill [definition, in RegLang.shepherdson]
DFA2.char [variable, in RegLang.two_way]
DFA2.M [variable, in RegLang.two_way]
dir [definition, in RegLang.two_way]
dlang [definition, in RegLang.languages]
drop_accept [lemma, in RegLang.two_way]
E
edges [definition, in RegLang.regexp]edgesP [definition, in RegLang.regexp]
empty [definition, in RegLang.wmso]
enfa [record, in RegLang.nfa]
enfaE [lemma, in RegLang.nfa]
EnfaFin [constructor, in RegLang.nfa]
EnfaNone [constructor, in RegLang.nfa]
EnfaSome [constructor, in RegLang.nfa]
enfa_for_ltn [definition, in RegLang.wmso]
enfa_starP [lemma, in RegLang.nfa]
enfa_starE [lemma, in RegLang.nfa]
enfa_star_langI [lemma, in RegLang.nfa]
enfa_starI [lemma, in RegLang.nfa]
enfa_star_cat [lemma, in RegLang.nfa]
enfa_f_None [lemma, in RegLang.nfa]
enfa_s_None [lemma, in RegLang.nfa]
enfa_star [definition, in RegLang.nfa]
enfa_concP [lemma, in RegLang.nfa]
enfa_concIl [lemma, in RegLang.nfa]
enfa_concIr [lemma, in RegLang.nfa]
enfa_concE [lemma, in RegLang.nfa]
enfa_conc [definition, in RegLang.nfa]
enfa_lang [definition, in RegLang.nfa]
enfa_accept [inductive, in RegLang.nfa]
enfa_trans [projection, in RegLang.nfa]
enfa_f [projection, in RegLang.nfa]
enfa_s [projection, in RegLang.nfa]
enfa_state [projection, in RegLang.nfa]
epiK [lemma, in RegLang.misc]
eps [definition, in RegLang.languages]
Eps [constructor, in RegLang.regexp]
eps_reach [definition, in RegLang.nfa]
eqb_iff [lemma, in RegLang.misc]
eq_regexp_dec [lemma, in RegLang.regexp]
Ex [constructor, in RegLang.wmso]
exn [definition, in RegLang.wmso]
exseqb [definition, in RegLang.dfa]
exseqP [lemma, in RegLang.dfa]
exseq_dec [lemma, in RegLang.dfa]
Ex1 [definition, in RegLang.wmso]
ex1s [lemma, in RegLang.misc]
F
FA [section, in RegLang.dfa]FA.char [variable, in RegLang.dfa]
FA.CutOff [section, in RegLang.dfa]
FA.CutOff.aT [variable, in RegLang.dfa]
FA.CutOff.f [variable, in RegLang.dfa]
FA.CutOff.RC_f [variable, in RegLang.dfa]
FA.CutOff.rT [variable, in RegLang.dfa]
FA.DFAOps [section, in RegLang.dfa]
FA.DFAOps.A1 [variable, in RegLang.dfa]
FA.DFAOps.A2 [variable, in RegLang.dfa]
FA.DFAOps.op [variable, in RegLang.dfa]
FA.DFA_Acceptance.A [variable, in RegLang.dfa]
FA.DFA_Acceptance [section, in RegLang.dfa]
FA.Emptyness [section, in RegLang.dfa]
FA.Emptyness.A [variable, in RegLang.dfa]
FF [constructor, in RegLang.wmso]
find_minn_bound [lemma, in RegLang.misc]
flatten_rcons [lemma, in RegLang.misc]
form [inductive, in RegLang.wmso]
form_ofP [lemma, in RegLang.wmso]
form_of [definition, in RegLang.wmso]
functional [definition, in RegLang.misc]
Functional [section, in RegLang.misc]
functional_srel [lemma, in RegLang.shepherdson]
functional_sub [lemma, in RegLang.misc]
Functional.e [variable, in RegLang.misc]
Functional.e' [variable, in RegLang.misc]
Functional.f [variable, in RegLang.misc]
Functional.f_inv [variable, in RegLang.misc]
Functional.f_eq [variable, in RegLang.misc]
Functional.f_inj [variable, in RegLang.misc]
Functional.T [variable, in RegLang.misc]
Functional.T' [variable, in RegLang.misc]
G
glue [definition, in RegLang.wmso]H
HomDef [section, in RegLang.languages]HomDef.char [variable, in RegLang.languages]
HomDef.char' [variable, in RegLang.languages]
HomDef.h [variable, in RegLang.languages]
HomDef.h_hom [variable, in RegLang.languages]
homomorphism [definition, in RegLang.languages]
h_flatten [lemma, in RegLang.languages]
h_seq [lemma, in RegLang.languages]
h0 [lemma, in RegLang.languages]
I
Iff [definition, in RegLang.wmso]IffT [constructor, in RegLang.misc]
iffT [inductive, in RegLang.misc]
iffT_RL [definition, in RegLang.misc]
iffT_LR [definition, in RegLang.misc]
image [definition, in RegLang.languages]
Image [section, in RegLang.regexp]
image_refines [lemma, in RegLang.shepherdson]
image_rc [lemma, in RegLang.shepherdson]
image_fun [definition, in RegLang.dfa]
image_fun_proof [lemma, in RegLang.dfa]
image_type [definition, in RegLang.dfa]
image_ext [lemma, in RegLang.languages]
Image.char [variable, in RegLang.regexp]
Image.char' [variable, in RegLang.regexp]
Image.h [variable, in RegLang.regexp]
Image.h_hom [variable, in RegLang.regexp]
imfun_of_congruent [lemma, in RegLang.myhill_nerode]
imfun_of_refines [lemma, in RegLang.myhill_nerode]
imfun_of_surj [definition, in RegLang.myhill_nerode]
imfun_of [definition, in RegLang.myhill_nerode]
Imp [constructor, in RegLang.wmso]
im_regular [lemma, in RegLang.regexp]
Incl [constructor, in RegLang.wmso]
index_take [lemma, in RegLang.misc]
init [definition, in RegLang.wmso]
inord_inj [lemma, in RegLang.shepherdson]
inord_max [lemma, in RegLang.misc]
inord0 [lemma, in RegLang.misc]
inord1 [lemma, in RegLang.misc]
Inter [definition, in RegLang.regexp]
Inter_correct [lemma, in RegLang.regexp]
iso [definition, in RegLang.minimization]
iso_inv [definition, in RegLang.minimization]
I_of_glueS [lemma, in RegLang.wmso]
I_of_glue0 [lemma, in RegLang.wmso]
I_of_vecP [lemma, in RegLang.wmso]
I_of_vev_max [lemma, in RegLang.wmso]
I_of [definition, in RegLang.wmso]
K
KleeneAlgorithm [section, in RegLang.regexp]KleeneAlgorithm.A [variable, in RegLang.regexp]
KleeneAlgorithm.c [variable, in RegLang.regexp]
KleeneAlgorithm.char [variable, in RegLang.regexp]
L^ _ [notation, in RegLang.regexp]
R^ _ [notation, in RegLang.regexp]
L
L [definition, in RegLang.two_way]L [definition, in RegLang.regexp]
Lab [definition, in RegLang.dfa]
Lab_not_regular [lemma, in RegLang.dfa]
Lab_eq [lemma, in RegLang.dfa]
lang [definition, in RegLang.languages]
Language [section, in RegLang.wmso]
languages [library]
Language.char [variable, in RegLang.wmso]
Leb [constructor, in RegLang.setoid_leq]
leb [inductive, in RegLang.setoid_leq]
leb_eq [lemma, in RegLang.setoid_leq]
LeftQuotient [section, in RegLang.dfa]
LeftQuotient.A [variable, in RegLang.dfa]
LeftQuotient.acc_L2 [variable, in RegLang.dfa]
LeftQuotient.A_start [variable, in RegLang.dfa]
LeftQuotient.char [variable, in RegLang.dfa]
LeftQuotient.dec_L1 [variable, in RegLang.dfa]
LeftQuotient.L1 [variable, in RegLang.dfa]
LeftQuotient.L2 [variable, in RegLang.dfa]
Leq [definition, in RegLang.wmso]
leqRW [definition, in RegLang.setoid_leq]
Less [constructor, in RegLang.wmso]
lift_accept [lemma, in RegLang.nfa]
lim [definition, in RegLang.wmso]
LP [lemma, in RegLang.regexp]
L_R [lemma, in RegLang.regexp]
L_rec [lemma, in RegLang.regexp]
L_star [lemma, in RegLang.regexp]
L_catR [lemma, in RegLang.regexp]
L_catL [lemma, in RegLang.regexp]
L_cat [lemma, in RegLang.regexp]
L_split [lemma, in RegLang.regexp]
L_set0 [lemma, in RegLang.regexp]
L_nil [lemma, in RegLang.regexp]
L_monotone [lemma, in RegLang.regexp]
M
max [definition, in RegLang.wmso]max_mem [lemma, in RegLang.misc]
mem_I_of [lemma, in RegLang.wmso]
mem_R0 [lemma, in RegLang.regexp]
mgClassifier [record, in RegLang.myhill_nerode]
mg_eq [definition, in RegLang.myhill_nerode]
mg_eq_proof [lemma, in RegLang.myhill_nerode]
mg_minimal [lemma, in RegLang.myhill_nerode]
mg_to_connected [lemma, in RegLang.myhill_nerode]
mg_to_dfa_correct [lemma, in RegLang.myhill_nerode]
mg_to_dfa [definition, in RegLang.myhill_nerode]
mg_to_classifier [definition, in RegLang.myhill_nerode]
mg_refines [lemma, in RegLang.myhill_nerode]
mg_right_congruent [lemma, in RegLang.myhill_nerode]
mg_classifier [projection, in RegLang.myhill_nerode]
minimal [definition, in RegLang.minimization]
minimalP [lemma, in RegLang.minimization]
minimal_iso [lemma, in RegLang.minimization]
minimal_collapsed [lemma, in RegLang.minimization]
minimal_connected [lemma, in RegLang.minimization]
minimal_classifier [definition, in RegLang.myhill_nerode]
minimal_nerode [lemma, in RegLang.myhill_nerode]
Minimization [section, in RegLang.minimization]
minimization [library]
Minimization.char [variable, in RegLang.minimization]
Minimization.Collapse [section, in RegLang.minimization]
Minimization.Collapse.A [variable, in RegLang.minimization]
Minimization.Isomopism [section, in RegLang.minimization]
Minimization.Isomopism.A [variable, in RegLang.minimization]
Minimization.Isomopism.A_conn [variable, in RegLang.minimization]
Minimization.Isomopism.A_coll [variable, in RegLang.minimization]
Minimization.Isomopism.B [variable, in RegLang.minimization]
Minimization.Isomopism.B_conn [variable, in RegLang.minimization]
Minimization.Isomopism.B_coll [variable, in RegLang.minimization]
Minimization.Isomopism.L_AB [variable, in RegLang.minimization]
Minimization.Prune [section, in RegLang.minimization]
Minimization.Prune.A [variable, in RegLang.minimization]
minimize [definition, in RegLang.minimization]
minimize_minimal [lemma, in RegLang.minimization]
minimize_correct [lemma, in RegLang.minimization]
minimize_connected [lemma, in RegLang.minimization]
minimize_collapsed [lemma, in RegLang.minimization]
minimize_size [lemma, in RegLang.minimization]
misc [library]
mso_regular [lemma, in RegLang.wmso]
mso_dec [lemma, in RegLang.wmso]
mso_preim [lemma, in RegLang.wmso]
mso_lang [definition, in RegLang.wmso]
myhill_nerode [library]
N
nat_succ [lemma, in RegLang.wmso]Neg [definition, in RegLang.regexp]
Neg_correct [lemma, in RegLang.regexp]
nerode [definition, in RegLang.myhill_nerode]
nerodeP [projection, in RegLang.myhill_nerode]
nfa [record, in RegLang.nfa]
NFA [section, in RegLang.nfa]
nfa [library]
nfaP [lemma, in RegLang.nfa]
NFAtoMSO [section, in RegLang.wmso]
NFAtoMSO.A [variable, in RegLang.wmso]
NFAtoMSO.n [variable, in RegLang.wmso]
NFAtoMSO.T [variable, in RegLang.wmso]
nfa_of_form_correct [lemma, in RegLang.wmso]
nfa_for_ltn_correct [lemma, in RegLang.wmso]
nfa_for_ltnP [lemma, in RegLang.wmso]
nfa_for_incl_correct [lemma, in RegLang.wmso]
nfa_for_ex_correct [lemma, in RegLang.wmso]
nfa_for_exE [lemma, in RegLang.wmso]
nfa_for_exI [lemma, in RegLang.wmso]
nfa_of_form [definition, in RegLang.wmso]
nfa_for_ex [definition, in RegLang.wmso]
nfa_for_ltn [definition, in RegLang.wmso]
nfa_for_incl [definition, in RegLang.wmso]
nfa_for_imp [definition, in RegLang.wmso]
nfa_for_bot [definition, in RegLang.wmso]
nfa_of_correct [lemma, in RegLang.vardi]
nfa_ofP [lemma, in RegLang.vardi]
nfa_of [definition, in RegLang.vardi]
nfa_regular [lemma, in RegLang.nfa]
nfa_inhabP [lemma, in RegLang.nfa]
nfa_inhab [definition, in RegLang.nfa]
nfa_acceptP [lemma, in RegLang.nfa]
nfa_run [inductive, in RegLang.nfa]
nfa_star_correct [lemma, in RegLang.nfa]
nfa_star [definition, in RegLang.nfa]
nfa_conc_correct [lemma, in RegLang.nfa]
nfa_conc [definition, in RegLang.nfa]
nfa_eps_correct [lemma, in RegLang.nfa]
nfa_eps [definition, in RegLang.nfa]
nfa_plus_correct [lemma, in RegLang.nfa]
nfa_plus [definition, in RegLang.nfa]
nfa_char_correct [lemma, in RegLang.nfa]
nfa_char [definition, in RegLang.nfa]
nfa_to_dfa_correct [lemma, in RegLang.nfa]
nfa_to_dfa [definition, in RegLang.nfa]
nfa_ofP [lemma, in RegLang.nfa]
nfa_of [definition, in RegLang.nfa]
nfa_lang [definition, in RegLang.nfa]
nfa_accept [definition, in RegLang.nfa]
nfa_trans [projection, in RegLang.nfa]
nfa_fin [projection, in RegLang.nfa]
nfa_s [projection, in RegLang.nfa]
nfa_state [projection, in RegLang.nfa]
NFA.char [variable, in RegLang.nfa]
NFA.Embed [section, in RegLang.nfa]
NFA.Embed.A [variable, in RegLang.nfa]
NFA.eNFAOps [section, in RegLang.nfa]
NFA.eNFAOps.A1 [variable, in RegLang.nfa]
NFA.eNFAOps.A2 [variable, in RegLang.nfa]
NFA.EpsilonNFA [section, in RegLang.nfa]
NFA.EpsilonNFA.N [variable, in RegLang.nfa]
NFA.NFARun [section, in RegLang.nfa]
NFA.NFARun.M [variable, in RegLang.nfa]
NFA.PowersetConstruction [section, in RegLang.nfa]
NFA.PowersetConstruction.A [variable, in RegLang.nfa]
nfa2 [record, in RegLang.two_way]
Nfa2 [constructor, in RegLang.two_way]
NFA2 [section, in RegLang.two_way]
NFA2toAFA [section, in RegLang.shepherdson]
NFA2toAFA.char [variable, in RegLang.shepherdson]
NFA2toAFA.CompositeWord [section, in RegLang.shepherdson]
NFA2toAFA.CompositeWord.x [variable, in RegLang.shepherdson]
NFA2toAFA.CompositeWord.z [variable, in RegLang.shepherdson]
NFA2toAFA.M [variable, in RegLang.shepherdson]
nfa2_of_dfa_det [lemma, in RegLang.two_way]
nfa2_of_correct [lemma, in RegLang.two_way]
nfa2_of_aux2 [lemma, in RegLang.two_way]
nfa2_of_aux [lemma, in RegLang.two_way]
nfa2_of_dfa [definition, in RegLang.two_way]
nfa2_of [projection, in RegLang.two_way]
nfa2_lang [definition, in RegLang.two_way]
nfa2_config [definition, in RegLang.two_way]
nfa2_transR [projection, in RegLang.two_way]
nfa2_transL [projection, in RegLang.two_way]
nfa2_trans [projection, in RegLang.two_way]
nfa2_f [projection, in RegLang.two_way]
nfa2_s [projection, in RegLang.two_way]
nfa2_state [projection, in RegLang.two_way]
nfa2_to_dfa [lemma, in RegLang.shepherdson]
nfa2_to_classifier [definition, in RegLang.shepherdson]
NFA2.A [variable, in RegLang.two_way]
NFA2.char [variable, in RegLang.two_way]
NFA2.x [variable, in RegLang.two_way]
NonRegular [section, in RegLang.dfa]
NonRegular.a [variable, in RegLang.dfa]
NonRegular.b [variable, in RegLang.dfa]
NonRegular.char [variable, in RegLang.dfa]
NonRegular.Hab [variable, in RegLang.dfa]
Not [definition, in RegLang.wmso]
nth_glueS [lemma, in RegLang.wmso]
nth_glue0 [lemma, in RegLang.wmso]
nth_cons [lemma, in RegLang.misc]
O
Or [definition, in RegLang.wmso]ord1 [definition, in RegLang.misc]
Ord2C [constructor, in RegLang.two_way]
Ord2M [constructor, in RegLang.two_way]
ord2P [lemma, in RegLang.two_way]
ord2PC [lemma, in RegLang.two_way]
ord2PM [lemma, in RegLang.two_way]
ord2P0 [lemma, in RegLang.two_way]
ord2_spec [inductive, in RegLang.two_way]
Ord20 [constructor, in RegLang.two_way]
orS [lemma, in RegLang.misc]
P
part [definition, in RegLang.wmso]plus [definition, in RegLang.languages]
Plus [constructor, in RegLang.regexp]
plusP [lemma, in RegLang.languages]
pos [definition, in RegLang.two_way]
Preimage [section, in RegLang.dfa]
preimage [definition, in RegLang.languages]
Preimage.char [variable, in RegLang.dfa]
Preimage.char' [variable, in RegLang.dfa]
Preimage.h [variable, in RegLang.dfa]
Preimage.h_hom [variable, in RegLang.dfa]
preim_regular [lemma, in RegLang.dfa]
prj_glue [lemma, in RegLang.wmso]
prj0 [definition, in RegLang.wmso]
prod [definition, in RegLang.languages]
prune_eq_connected [lemma, in RegLang.minimization]
pumping [lemma, in RegLang.dfa]
Pumping [section, in RegLang.dfa]
Pumping.char [variable, in RegLang.dfa]
pump_Lab [definition, in RegLang.dfa]
pump_dfa [lemma, in RegLang.dfa]
Q
quotL [definition, in RegLang.dfa]quotR [definition, in RegLang.dfa]
R
R [definition, in RegLang.two_way]R [definition, in RegLang.regexp]
rank [abbreviation, in RegLang.wmso]
RC_rep [lemma, in RegLang.dfa]
RC_seq [lemma, in RegLang.dfa]
reachabe_s_proof [lemma, in RegLang.minimization]
reachable [definition, in RegLang.minimization]
reachable_s [definition, in RegLang.minimization]
reachable_trans [definition, in RegLang.minimization]
reachable_trans_proof [lemma, in RegLang.minimization]
reachable_type [definition, in RegLang.minimization]
read [definition, in RegLang.two_way]
readL [lemma, in RegLang.shepherdson]
readR [lemma, in RegLang.shepherdson]
read1 [lemma, in RegLang.two_way]
refines [definition, in RegLang.myhill_nerode]
regexp [inductive, in RegLang.regexp]
RegExp [section, in RegLang.regexp]
regexp [library]
regexp_eqMixin [definition, in RegLang.regexp]
RegExp.char [variable, in RegLang.regexp]
regular [definition, in RegLang.dfa]
regularP [lemma, in RegLang.regexp]
regularU [lemma, in RegLang.dfa]
regular_xm [lemma, in RegLang.dfa]
regular_det [lemma, in RegLang.dfa]
regular_quotL [lemma, in RegLang.dfa]
regular_quotL_aux [lemma, in RegLang.dfa]
regular_quotR [lemma, in RegLang.dfa]
regular_bigU [lemma, in RegLang.dfa]
regular_inter [lemma, in RegLang.dfa]
regular_ext [lemma, in RegLang.dfa]
regular_rev [lemma, in RegLang.regexp]
regular0 [lemma, in RegLang.dfa]
reject_cert [definition, in RegLang.vardi]
rep [definition, in RegLang.dfa]
residual [definition, in RegLang.dfa]
residual [definition, in RegLang.languages]
residualP [lemma, in RegLang.dfa]
Rev [definition, in RegLang.regexp]
rev_flatten [lemma, in RegLang.misc]
Rev_correct [lemma, in RegLang.regexp]
re_imageP [lemma, in RegLang.regexp]
re_image [definition, in RegLang.regexp]
re_equiv_correct [lemma, in RegLang.regexp]
re_equiv [definition, in RegLang.regexp]
re_to_dfa_size [lemma, in RegLang.regexp]
re_to_dfa_correct [lemma, in RegLang.regexp]
re_to_dfa [definition, in RegLang.regexp]
re_to_nfa_size [lemma, in RegLang.regexp]
re_to_nfa_correct [lemma, in RegLang.regexp]
re_to_nfa [definition, in RegLang.regexp]
re_size [definition, in RegLang.regexp]
re_lang [definition, in RegLang.regexp]
RightQuotient [section, in RegLang.dfa]
RightQuotient.A [variable, in RegLang.dfa]
RightQuotient.acc_L1 [variable, in RegLang.dfa]
RightQuotient.char [variable, in RegLang.dfa]
RightQuotient.dec_L2 [variable, in RegLang.dfa]
RightQuotient.L1 [variable, in RegLang.dfa]
RightQuotient.L2 [variable, in RegLang.dfa]
right_congruent [definition, in RegLang.myhill_nerode]
run [definition, in RegLang.wmso]
runI [lemma, in RegLang.nfa]
runL [lemma, in RegLang.shepherdson]
runR [lemma, in RegLang.shepherdson]
runR_eq [lemma, in RegLang.shepherdson]
runS [constructor, in RegLang.nfa]
run_table [definition, in RegLang.vardi]
run_trans [lemma, in RegLang.nfa]
run_last [lemma, in RegLang.nfa]
run_size [lemma, in RegLang.nfa]
run0 [constructor, in RegLang.nfa]
R_size_high [lemma, in RegLang.regexp]
R_size_low [lemma, in RegLang.regexp]
R_size [lemma, in RegLang.regexp]
R_size_rec [definition, in RegLang.regexp]
R0 [definition, in RegLang.regexp]
R0_size [lemma, in RegLang.regexp]
S
satDN [lemma, in RegLang.wmso]satisfies [definition, in RegLang.wmso]
satisfies_dec [lemma, in RegLang.wmso]
satNNPP [lemma, in RegLang.wmso]
sat_accept [lemma, in RegLang.wmso]
sat_init [lemma, in RegLang.wmso]
sat_run [lemma, in RegLang.wmso]
sat_part [lemma, in RegLang.wmso]
sat_max [lemma, in RegLang.wmso]
sat_exn [lemma, in RegLang.wmso]
sat_leq [lemma, in RegLang.wmso]
sat_zero [lemma, in RegLang.wmso]
sat_succ [lemma, in RegLang.wmso]
sat_ex1 [lemma, in RegLang.wmso]
sat_all1 [lemma, in RegLang.wmso]
sat_bigand [lemma, in RegLang.wmso]
sat_orE [lemma, in RegLang.wmso]
sat_orI [lemma, in RegLang.wmso]
sat_singles [lemma, in RegLang.wmso]
sat_emptyN [lemma, in RegLang.wmso]
sat_empty [lemma, in RegLang.wmso]
sat_all [lemma, in RegLang.wmso]
sat_or [lemma, in RegLang.wmso]
sat_and [lemma, in RegLang.wmso]
sat_true [lemma, in RegLang.wmso]
sat_not [lemma, in RegLang.wmso]
sat_imp [lemma, in RegLang.wmso]
seq1P [lemma, in RegLang.misc]
setoid_leq [library]
set_enum [lemma, in RegLang.misc]
shepherdson [library]
single [definition, in RegLang.wmso]
size_glue [lemma, in RegLang.wmso]
size_induction [lemma, in RegLang.misc]
srel [definition, in RegLang.shepherdson]
srelL [lemma, in RegLang.shepherdson]
srelLR [lemma, in RegLang.shepherdson]
srelR [lemma, in RegLang.shepherdson]
srelRE [lemma, in RegLang.shepherdson]
srelS [lemma, in RegLang.shepherdson]
srelSr [lemma, in RegLang.shepherdson]
srel_mid [lemma, in RegLang.shepherdson]
srel_mid_path [lemma, in RegLang.shepherdson]
srel_step_max [lemma, in RegLang.shepherdson]
srel_step [lemma, in RegLang.shepherdson]
srel1 [lemma, in RegLang.shepherdson]
star [definition, in RegLang.languages]
Star [constructor, in RegLang.regexp]
starI [lemma, in RegLang.languages]
starP [lemma, in RegLang.languages]
star_eq [lemma, in RegLang.languages]
star_cat [lemma, in RegLang.languages]
step [definition, in RegLang.two_way]
step_fun [lemma, in RegLang.two_way]
String [definition, in RegLang.regexp]
StringE [lemma, in RegLang.regexp]
sub [definition, in RegLang.dfa]
Sub_eq [lemma, in RegLang.misc]
sub_exists [lemma, in RegLang.misc]
sub_forall [lemma, in RegLang.misc]
sub_run [lemma, in RegLang.vardi]
sub1P [lemma, in RegLang.misc]
succ [definition, in RegLang.wmso]
surjective [definition, in RegLang.misc]
surjectiveE [lemma, in RegLang.misc]
surjective_image_fun [lemma, in RegLang.dfa]
surj_card_bij [lemma, in RegLang.misc]
T
Tab [definition, in RegLang.shepherdson]table [definition, in RegLang.shepherdson]
Tab_rc [lemma, in RegLang.shepherdson]
Tab_refines [lemma, in RegLang.shepherdson]
Tab' [definition, in RegLang.shepherdson]
Tab1P [lemma, in RegLang.shepherdson]
Tab1_uniq [lemma, in RegLang.shepherdson]
Tab2P [lemma, in RegLang.shepherdson]
Tab2_functional [lemma, in RegLang.shepherdson]
take_addn [lemma, in RegLang.misc]
take_take [lemma, in RegLang.misc]
tape [definition, in RegLang.two_way]
terminal [definition, in RegLang.misc]
term_srel [lemma, in RegLang.shepherdson]
term_uniq [lemma, in RegLang.misc]
tnthL [lemma, in RegLang.shepherdson]
tnthR [lemma, in RegLang.shepherdson]
trans_b0 [definition, in RegLang.wmso]
TT [definition, in RegLang.wmso]
two_way [library]
T1 [lemma, in RegLang.setoid_leq]
T2 [lemma, in RegLang.setoid_leq]
V
val [abbreviation, in RegLang.wmso]valuation [definition, in RegLang.wmso]
Vardi [section, in RegLang.vardi]
vardi [library]
Vardi.char [variable, in RegLang.vardi]
Vardi.Completeness [section, in RegLang.vardi]
Vardi.Completeness.a [variable, in RegLang.vardi]
Vardi.Completeness.U [variable, in RegLang.vardi]
Vardi.Completeness.V [variable, in RegLang.vardi]
Vardi.Completeness.W [variable, in RegLang.vardi]
Vardi.M [variable, in RegLang.vardi]
vec [abbreviation, in RegLang.wmso]
vec_lang_regular [lemma, in RegLang.wmso]
vec_of_valP [lemma, in RegLang.wmso]
vec_of_val_agrees [lemma, in RegLang.wmso]
vec_of_val [definition, in RegLang.wmso]
vec_Ex_prj0 [lemma, in RegLang.wmso]
vec_lang0 [lemma, in RegLang.wmso]
vec_ex_glue [lemma, in RegLang.wmso]
vec_of_hom [lemma, in RegLang.wmso]
vec_lang [definition, in RegLang.wmso]
vec_of [definition, in RegLang.wmso]
void [definition, in RegLang.languages]
Void [constructor, in RegLang.regexp]
W
weak_coincidence [lemma, in RegLang.wmso]wmso [library]
word [abbreviation, in RegLang.dfa]
word [definition, in RegLang.languages]
word [abbreviation, in RegLang.minimization]
word [abbreviation, in RegLang.myhill_nerode]
word [abbreviation, in RegLang.nfa]
Z
zero [definition, in RegLang.wmso]zero_at [definition, in RegLang.wmso]
other
_ <--> _ [notation, in RegLang.wmso]_ :\/: _ [notation, in RegLang.wmso]
_ :/\: _ [notation, in RegLang.wmso]
_ --> _ [notation, in RegLang.wmso]
_ |= _ [notation, in RegLang.wmso]
_ <-T-> _ [notation, in RegLang.misc]
_ =p _ [notation, in RegLang.misc]
Eps [notation, in RegLang.regexp]
Void [notation, in RegLang.regexp]
\and_ ( _ \in _ ) _ [notation, in RegLang.wmso]
\and_ ( _ <- _ ) _ [notation, in RegLang.wmso]
\or_ ( _ \in _ ) _ [notation, in RegLang.wmso]
\or_ ( _ <- _ ) _ [notation, in RegLang.wmso]
\sigma_( _ | _ ) _ [notation, in RegLang.regexp]
\sigma_( _ <- _ ) _ [notation, in RegLang.regexp]
Notation Index
K
L^ _ [in RegLang.regexp]R^ _ [in RegLang.regexp]
other
_ <--> _ [in RegLang.wmso]_ :\/: _ [in RegLang.wmso]
_ :/\: _ [in RegLang.wmso]
_ --> _ [in RegLang.wmso]
_ |= _ [in RegLang.wmso]
_ <-T-> _ [in RegLang.misc]
_ =p _ [in RegLang.misc]
Eps [in RegLang.regexp]
Void [in RegLang.regexp]
\and_ ( _ \in _ ) _ [in RegLang.wmso]
\and_ ( _ <- _ ) _ [in RegLang.wmso]
\or_ ( _ \in _ ) _ [in RegLang.wmso]
\or_ ( _ <- _ ) _ [in RegLang.wmso]
\sigma_( _ | _ ) _ [in RegLang.regexp]
\sigma_( _ <- _ ) _ [in RegLang.regexp]
Variable Index
B
Basics.char [in RegLang.languages]C
Clasifiers.char [in RegLang.myhill_nerode]Clasifiers.ClassifierToDFA.L [in RegLang.myhill_nerode]
Clasifiers.ClassifierToDFA.M [in RegLang.myhill_nerode]
Clasifiers.DFAtoClassifier.A [in RegLang.myhill_nerode]
Clasifiers.mDFAtoMG.A [in RegLang.myhill_nerode]
Clasifiers.mDFAtoMG.MA [in RegLang.myhill_nerode]
D
DecidableLanguages.char [in RegLang.languages]DFAofRE.char [in RegLang.regexp]
DFAtoDFA2.A [in RegLang.two_way]
DFAtoDFA2.char [in RegLang.two_way]
DFAtoDFA2.n [in RegLang.two_way]
DFAtoDFA2.w [in RegLang.two_way]
DFA2toAFA.char [in RegLang.shepherdson]
DFA2toAFA.M [in RegLang.shepherdson]
DFA2.char [in RegLang.two_way]
DFA2.M [in RegLang.two_way]
F
FA.char [in RegLang.dfa]FA.CutOff.aT [in RegLang.dfa]
FA.CutOff.f [in RegLang.dfa]
FA.CutOff.RC_f [in RegLang.dfa]
FA.CutOff.rT [in RegLang.dfa]
FA.DFAOps.A1 [in RegLang.dfa]
FA.DFAOps.A2 [in RegLang.dfa]
FA.DFAOps.op [in RegLang.dfa]
FA.DFA_Acceptance.A [in RegLang.dfa]
FA.Emptyness.A [in RegLang.dfa]
Functional.e [in RegLang.misc]
Functional.e' [in RegLang.misc]
Functional.f [in RegLang.misc]
Functional.f_inv [in RegLang.misc]
Functional.f_eq [in RegLang.misc]
Functional.f_inj [in RegLang.misc]
Functional.T [in RegLang.misc]
Functional.T' [in RegLang.misc]
H
HomDef.char [in RegLang.languages]HomDef.char' [in RegLang.languages]
HomDef.h [in RegLang.languages]
HomDef.h_hom [in RegLang.languages]
I
Image.char [in RegLang.regexp]Image.char' [in RegLang.regexp]
Image.h [in RegLang.regexp]
Image.h_hom [in RegLang.regexp]
K
KleeneAlgorithm.A [in RegLang.regexp]KleeneAlgorithm.c [in RegLang.regexp]
KleeneAlgorithm.char [in RegLang.regexp]
L
Language.char [in RegLang.wmso]LeftQuotient.A [in RegLang.dfa]
LeftQuotient.acc_L2 [in RegLang.dfa]
LeftQuotient.A_start [in RegLang.dfa]
LeftQuotient.char [in RegLang.dfa]
LeftQuotient.dec_L1 [in RegLang.dfa]
LeftQuotient.L1 [in RegLang.dfa]
LeftQuotient.L2 [in RegLang.dfa]
M
Minimization.char [in RegLang.minimization]Minimization.Collapse.A [in RegLang.minimization]
Minimization.Isomopism.A [in RegLang.minimization]
Minimization.Isomopism.A_conn [in RegLang.minimization]
Minimization.Isomopism.A_coll [in RegLang.minimization]
Minimization.Isomopism.B [in RegLang.minimization]
Minimization.Isomopism.B_conn [in RegLang.minimization]
Minimization.Isomopism.B_coll [in RegLang.minimization]
Minimization.Isomopism.L_AB [in RegLang.minimization]
Minimization.Prune.A [in RegLang.minimization]
N
NFAtoMSO.A [in RegLang.wmso]NFAtoMSO.n [in RegLang.wmso]
NFAtoMSO.T [in RegLang.wmso]
NFA.char [in RegLang.nfa]
NFA.Embed.A [in RegLang.nfa]
NFA.eNFAOps.A1 [in RegLang.nfa]
NFA.eNFAOps.A2 [in RegLang.nfa]
NFA.EpsilonNFA.N [in RegLang.nfa]
NFA.NFARun.M [in RegLang.nfa]
NFA.PowersetConstruction.A [in RegLang.nfa]
NFA2toAFA.char [in RegLang.shepherdson]
NFA2toAFA.CompositeWord.x [in RegLang.shepherdson]
NFA2toAFA.CompositeWord.z [in RegLang.shepherdson]
NFA2toAFA.M [in RegLang.shepherdson]
NFA2.A [in RegLang.two_way]
NFA2.char [in RegLang.two_way]
NFA2.x [in RegLang.two_way]
NonRegular.a [in RegLang.dfa]
NonRegular.b [in RegLang.dfa]
NonRegular.char [in RegLang.dfa]
NonRegular.Hab [in RegLang.dfa]
P
Preimage.char [in RegLang.dfa]Preimage.char' [in RegLang.dfa]
Preimage.h [in RegLang.dfa]
Preimage.h_hom [in RegLang.dfa]
Pumping.char [in RegLang.dfa]
R
RegExp.char [in RegLang.regexp]RightQuotient.A [in RegLang.dfa]
RightQuotient.acc_L1 [in RegLang.dfa]
RightQuotient.char [in RegLang.dfa]
RightQuotient.dec_L2 [in RegLang.dfa]
RightQuotient.L1 [in RegLang.dfa]
RightQuotient.L2 [in RegLang.dfa]
V
Vardi.char [in RegLang.vardi]Vardi.Completeness.a [in RegLang.vardi]
Vardi.Completeness.U [in RegLang.vardi]
Vardi.Completeness.V [in RegLang.vardi]
Vardi.Completeness.W [in RegLang.vardi]
Vardi.M [in RegLang.vardi]
Library Index
D
dfaL
languagesM
minimizationmisc
myhill_nerode
N
nfaR
regexpS
setoid_leqshepherdson
T
two_wayV
vardiW
wmsoLemma Index
A
abstract_minimization [in RegLang.minimization]accept_cons [in RegLang.dfa]
accept_nil [in RegLang.dfa]
agree_dc [in RegLang.wmso]
allseq_dec [in RegLang.dfa]
all1s [in RegLang.misc]
all1sT [in RegLang.misc]
A_start_cat [in RegLang.dfa]
B
behead_cons [in RegLang.wmso]bigmax_seq_sup [in RegLang.misc]
big_plus_size [in RegLang.regexp]
big_plusP [in RegLang.regexp]
big_plus_seqP [in RegLang.regexp]
bij_card [in RegLang.misc]
C
can_iso_inv [in RegLang.minimization]can_iso [in RegLang.minimization]
cards_lt1 [in RegLang.two_way]
cardT_eq [in RegLang.misc]
card_set [in RegLang.misc]
card_leq_inj [in RegLang.misc]
cat_size [in RegLang.wmso]
cat_beyond [in RegLang.wmso]
cat_prefix [in RegLang.wmso]
cat_nseq_eq [in RegLang.dfa]
cf_lang_eq_proof [in RegLang.myhill_nerode]
classifier_to_dfa_connected [in RegLang.myhill_nerode]
classifier_to_dfa_correct [in RegLang.myhill_nerode]
classifier_to_dfa_delta [in RegLang.myhill_nerode]
coincidence [in RegLang.wmso]
collapse_connected [in RegLang.minimization]
collapse_size [in RegLang.minimization]
collapse_correct [in RegLang.minimization]
collapse_collapsed [in RegLang.minimization]
collapse_fin [in RegLang.minimization]
collapse_delta [in RegLang.minimization]
collb_step [in RegLang.minimization]
collb_trans [in RegLang.minimization]
collb_sym [in RegLang.minimization]
collb_refl [in RegLang.minimization]
collP [in RegLang.minimization]
coll_fun_RC [in RegLang.minimization]
coll_iso [in RegLang.minimization]
concP [in RegLang.languages]
conc_eq [in RegLang.languages]
conc_cat [in RegLang.languages]
connectedP [in RegLang.minimization]
connect_transfer [in RegLang.misc]
contraN [in RegLang.shepherdson]
countL [in RegLang.dfa]
countR [in RegLang.dfa]
count_nseq [in RegLang.dfa]
crK [in RegLang.misc]
D
dec_eq [in RegLang.misc]dec_iff [in RegLang.misc]
delta_rep [in RegLang.dfa]
delta_rc [in RegLang.dfa]
delta_lang [in RegLang.dfa]
delta_cat [in RegLang.dfa]
delta_cons [in RegLang.dfa]
delta_iso_inv [in RegLang.minimization]
delta_iso [in RegLang.minimization]
delta_s_refines [in RegLang.myhill_nerode]
delta_s_right_congruent [in RegLang.myhill_nerode]
det_range [in RegLang.shepherdson]
dfa_quotP [in RegLang.dfa]
dfa_preimP [in RegLang.dfa]
dfa_incl_correct [in RegLang.dfa]
dfa_equiv_correct [in RegLang.dfa]
dfa_emptyP [in RegLang.dfa]
dfa_inhabP [in RegLang.dfa]
dfa_op_correct [in RegLang.dfa]
dfa_compl_correct [in RegLang.dfa]
dfa_void_correct [in RegLang.dfa]
dfa_prune_size [in RegLang.minimization]
dfa_prune_connected [in RegLang.minimization]
dfa_prune_correct [in RegLang.minimization]
dfa_iso_size [in RegLang.minimization]
dfa_to_re_size [in RegLang.regexp]
dfa_to_re_correct [in RegLang.regexp]
dfa_L [in RegLang.regexp]
dfa_to_cf_size [in RegLang.myhill_nerode]
dfa_to_nfa_correct [in RegLang.nfa]
dfa0_correct [in RegLang.dfa]
dfa2Pn [in RegLang.vardi]
dfa2_of_correct [in RegLang.two_way]
dfa2_to_dfa [in RegLang.shepherdson]
drop_accept [in RegLang.two_way]
E
enfaE [in RegLang.nfa]enfa_starP [in RegLang.nfa]
enfa_starE [in RegLang.nfa]
enfa_star_langI [in RegLang.nfa]
enfa_starI [in RegLang.nfa]
enfa_star_cat [in RegLang.nfa]
enfa_f_None [in RegLang.nfa]
enfa_s_None [in RegLang.nfa]
enfa_concP [in RegLang.nfa]
enfa_concIl [in RegLang.nfa]
enfa_concIr [in RegLang.nfa]
enfa_concE [in RegLang.nfa]
epiK [in RegLang.misc]
eqb_iff [in RegLang.misc]
eq_regexp_dec [in RegLang.regexp]
exseqP [in RegLang.dfa]
exseq_dec [in RegLang.dfa]
ex1s [in RegLang.misc]
F
find_minn_bound [in RegLang.misc]flatten_rcons [in RegLang.misc]
form_ofP [in RegLang.wmso]
functional_srel [in RegLang.shepherdson]
functional_sub [in RegLang.misc]
H
h_flatten [in RegLang.languages]h_seq [in RegLang.languages]
h0 [in RegLang.languages]
I
image_refines [in RegLang.shepherdson]image_rc [in RegLang.shepherdson]
image_fun_proof [in RegLang.dfa]
image_ext [in RegLang.languages]
imfun_of_congruent [in RegLang.myhill_nerode]
imfun_of_refines [in RegLang.myhill_nerode]
im_regular [in RegLang.regexp]
index_take [in RegLang.misc]
inord_inj [in RegLang.shepherdson]
inord_max [in RegLang.misc]
inord0 [in RegLang.misc]
inord1 [in RegLang.misc]
Inter_correct [in RegLang.regexp]
I_of_glueS [in RegLang.wmso]
I_of_glue0 [in RegLang.wmso]
I_of_vecP [in RegLang.wmso]
I_of_vev_max [in RegLang.wmso]
L
Lab_not_regular [in RegLang.dfa]Lab_eq [in RegLang.dfa]
leb_eq [in RegLang.setoid_leq]
lift_accept [in RegLang.nfa]
LP [in RegLang.regexp]
L_R [in RegLang.regexp]
L_rec [in RegLang.regexp]
L_star [in RegLang.regexp]
L_catR [in RegLang.regexp]
L_catL [in RegLang.regexp]
L_cat [in RegLang.regexp]
L_split [in RegLang.regexp]
L_set0 [in RegLang.regexp]
L_nil [in RegLang.regexp]
L_monotone [in RegLang.regexp]
M
max_mem [in RegLang.misc]mem_I_of [in RegLang.wmso]
mem_R0 [in RegLang.regexp]
mg_eq_proof [in RegLang.myhill_nerode]
mg_minimal [in RegLang.myhill_nerode]
mg_to_connected [in RegLang.myhill_nerode]
mg_to_dfa_correct [in RegLang.myhill_nerode]
mg_refines [in RegLang.myhill_nerode]
mg_right_congruent [in RegLang.myhill_nerode]
minimalP [in RegLang.minimization]
minimal_iso [in RegLang.minimization]
minimal_collapsed [in RegLang.minimization]
minimal_connected [in RegLang.minimization]
minimal_nerode [in RegLang.myhill_nerode]
minimize_minimal [in RegLang.minimization]
minimize_correct [in RegLang.minimization]
minimize_connected [in RegLang.minimization]
minimize_collapsed [in RegLang.minimization]
minimize_size [in RegLang.minimization]
mso_regular [in RegLang.wmso]
mso_dec [in RegLang.wmso]
mso_preim [in RegLang.wmso]
N
nat_succ [in RegLang.wmso]Neg_correct [in RegLang.regexp]
nfaP [in RegLang.nfa]
nfa_of_form_correct [in RegLang.wmso]
nfa_for_ltn_correct [in RegLang.wmso]
nfa_for_ltnP [in RegLang.wmso]
nfa_for_incl_correct [in RegLang.wmso]
nfa_for_ex_correct [in RegLang.wmso]
nfa_for_exE [in RegLang.wmso]
nfa_for_exI [in RegLang.wmso]
nfa_of_correct [in RegLang.vardi]
nfa_ofP [in RegLang.vardi]
nfa_regular [in RegLang.nfa]
nfa_inhabP [in RegLang.nfa]
nfa_acceptP [in RegLang.nfa]
nfa_star_correct [in RegLang.nfa]
nfa_conc_correct [in RegLang.nfa]
nfa_eps_correct [in RegLang.nfa]
nfa_plus_correct [in RegLang.nfa]
nfa_char_correct [in RegLang.nfa]
nfa_to_dfa_correct [in RegLang.nfa]
nfa_ofP [in RegLang.nfa]
nfa2_of_dfa_det [in RegLang.two_way]
nfa2_of_correct [in RegLang.two_way]
nfa2_of_aux2 [in RegLang.two_way]
nfa2_of_aux [in RegLang.two_way]
nfa2_to_dfa [in RegLang.shepherdson]
nth_glueS [in RegLang.wmso]
nth_glue0 [in RegLang.wmso]
nth_cons [in RegLang.misc]
O
ord2P [in RegLang.two_way]ord2PC [in RegLang.two_way]
ord2PM [in RegLang.two_way]
ord2P0 [in RegLang.two_way]
orS [in RegLang.misc]
P
plusP [in RegLang.languages]preim_regular [in RegLang.dfa]
prj_glue [in RegLang.wmso]
prune_eq_connected [in RegLang.minimization]
pumping [in RegLang.dfa]
pump_dfa [in RegLang.dfa]
R
RC_rep [in RegLang.dfa]RC_seq [in RegLang.dfa]
reachabe_s_proof [in RegLang.minimization]
reachable_trans_proof [in RegLang.minimization]
readL [in RegLang.shepherdson]
readR [in RegLang.shepherdson]
read1 [in RegLang.two_way]
regularP [in RegLang.regexp]
regularU [in RegLang.dfa]
regular_xm [in RegLang.dfa]
regular_det [in RegLang.dfa]
regular_quotL [in RegLang.dfa]
regular_quotL_aux [in RegLang.dfa]
regular_quotR [in RegLang.dfa]
regular_bigU [in RegLang.dfa]
regular_inter [in RegLang.dfa]
regular_ext [in RegLang.dfa]
regular_rev [in RegLang.regexp]
regular0 [in RegLang.dfa]
residualP [in RegLang.dfa]
rev_flatten [in RegLang.misc]
Rev_correct [in RegLang.regexp]
re_imageP [in RegLang.regexp]
re_equiv_correct [in RegLang.regexp]
re_to_dfa_size [in RegLang.regexp]
re_to_dfa_correct [in RegLang.regexp]
re_to_nfa_size [in RegLang.regexp]
re_to_nfa_correct [in RegLang.regexp]
runI [in RegLang.nfa]
runL [in RegLang.shepherdson]
runR [in RegLang.shepherdson]
runR_eq [in RegLang.shepherdson]
run_trans [in RegLang.nfa]
run_last [in RegLang.nfa]
run_size [in RegLang.nfa]
R_size_high [in RegLang.regexp]
R_size_low [in RegLang.regexp]
R_size [in RegLang.regexp]
R0_size [in RegLang.regexp]
S
satDN [in RegLang.wmso]satisfies_dec [in RegLang.wmso]
satNNPP [in RegLang.wmso]
sat_accept [in RegLang.wmso]
sat_init [in RegLang.wmso]
sat_run [in RegLang.wmso]
sat_part [in RegLang.wmso]
sat_max [in RegLang.wmso]
sat_exn [in RegLang.wmso]
sat_leq [in RegLang.wmso]
sat_zero [in RegLang.wmso]
sat_succ [in RegLang.wmso]
sat_ex1 [in RegLang.wmso]
sat_all1 [in RegLang.wmso]
sat_bigand [in RegLang.wmso]
sat_orE [in RegLang.wmso]
sat_orI [in RegLang.wmso]
sat_singles [in RegLang.wmso]
sat_emptyN [in RegLang.wmso]
sat_empty [in RegLang.wmso]
sat_all [in RegLang.wmso]
sat_or [in RegLang.wmso]
sat_and [in RegLang.wmso]
sat_true [in RegLang.wmso]
sat_not [in RegLang.wmso]
sat_imp [in RegLang.wmso]
seq1P [in RegLang.misc]
set_enum [in RegLang.misc]
size_glue [in RegLang.wmso]
size_induction [in RegLang.misc]
srelL [in RegLang.shepherdson]
srelLR [in RegLang.shepherdson]
srelR [in RegLang.shepherdson]
srelRE [in RegLang.shepherdson]
srelS [in RegLang.shepherdson]
srelSr [in RegLang.shepherdson]
srel_mid [in RegLang.shepherdson]
srel_mid_path [in RegLang.shepherdson]
srel_step_max [in RegLang.shepherdson]
srel_step [in RegLang.shepherdson]
srel1 [in RegLang.shepherdson]
starI [in RegLang.languages]
starP [in RegLang.languages]
star_eq [in RegLang.languages]
star_cat [in RegLang.languages]
step_fun [in RegLang.two_way]
StringE [in RegLang.regexp]
Sub_eq [in RegLang.misc]
sub_exists [in RegLang.misc]
sub_forall [in RegLang.misc]
sub_run [in RegLang.vardi]
sub1P [in RegLang.misc]
surjectiveE [in RegLang.misc]
surjective_image_fun [in RegLang.dfa]
surj_card_bij [in RegLang.misc]
T
Tab_rc [in RegLang.shepherdson]Tab_refines [in RegLang.shepherdson]
Tab1P [in RegLang.shepherdson]
Tab1_uniq [in RegLang.shepherdson]
Tab2P [in RegLang.shepherdson]
Tab2_functional [in RegLang.shepherdson]
take_addn [in RegLang.misc]
take_take [in RegLang.misc]
term_srel [in RegLang.shepherdson]
term_uniq [in RegLang.misc]
tnthL [in RegLang.shepherdson]
tnthR [in RegLang.shepherdson]
T1 [in RegLang.setoid_leq]
T2 [in RegLang.setoid_leq]
V
vec_lang_regular [in RegLang.wmso]vec_of_valP [in RegLang.wmso]
vec_of_val_agrees [in RegLang.wmso]
vec_Ex_prj0 [in RegLang.wmso]
vec_lang0 [in RegLang.wmso]
vec_ex_glue [in RegLang.wmso]
vec_of_hom [in RegLang.wmso]
W
weak_coincidence [in RegLang.wmso]Constructor Index
A
Atom [in RegLang.regexp]C
Classifier [in RegLang.myhill_nerode]Conc [in RegLang.regexp]
D
DFA2 [in RegLang.two_way]E
EnfaFin [in RegLang.nfa]EnfaNone [in RegLang.nfa]
EnfaSome [in RegLang.nfa]
Eps [in RegLang.regexp]
Ex [in RegLang.wmso]
F
FF [in RegLang.wmso]I
IffT [in RegLang.misc]Imp [in RegLang.wmso]
Incl [in RegLang.wmso]
L
Leb [in RegLang.setoid_leq]Less [in RegLang.wmso]
N
Nfa2 [in RegLang.two_way]O
Ord2C [in RegLang.two_way]Ord2M [in RegLang.two_way]
Ord20 [in RegLang.two_way]
P
Plus [in RegLang.regexp]R
runS [in RegLang.nfa]run0 [in RegLang.nfa]
S
Star [in RegLang.regexp]V
Void [in RegLang.regexp]Inductive Index
E
enfa_accept [in RegLang.nfa]F
form [in RegLang.wmso]I
iffT [in RegLang.misc]L
leb [in RegLang.setoid_leq]N
nfa_run [in RegLang.nfa]O
ord2_spec [in RegLang.two_way]R
regexp [in RegLang.regexp]Projection Index
C
cf_refines [in RegLang.myhill_nerode]cf_congruent [in RegLang.myhill_nerode]
cf_classifier [in RegLang.myhill_nerode]
classifier_fun [in RegLang.myhill_nerode]
classifier_classes [in RegLang.myhill_nerode]
D
detC [in RegLang.two_way]detL [in RegLang.two_way]
detR [in RegLang.two_way]
dfa_trans [in RegLang.dfa]
dfa_fin [in RegLang.dfa]
dfa_s [in RegLang.dfa]
dfa_state [in RegLang.dfa]
dfa2_det [in RegLang.two_way]
E
enfa_trans [in RegLang.nfa]enfa_f [in RegLang.nfa]
enfa_s [in RegLang.nfa]
enfa_state [in RegLang.nfa]
M
mg_classifier [in RegLang.myhill_nerode]N
nerodeP [in RegLang.myhill_nerode]nfa_trans [in RegLang.nfa]
nfa_fin [in RegLang.nfa]
nfa_s [in RegLang.nfa]
nfa_state [in RegLang.nfa]
nfa2_of [in RegLang.two_way]
nfa2_transR [in RegLang.two_way]
nfa2_transL [in RegLang.two_way]
nfa2_trans [in RegLang.two_way]
nfa2_f [in RegLang.two_way]
nfa2_s [in RegLang.two_way]
nfa2_state [in RegLang.two_way]
Section Index
B
Basics [in RegLang.languages]C
Clasifiers [in RegLang.myhill_nerode]Clasifiers.ClassifierToDFA [in RegLang.myhill_nerode]
Clasifiers.DFAtoClassifier [in RegLang.myhill_nerode]
Clasifiers.mDFAtoMG [in RegLang.myhill_nerode]
D
DecidableLanguages [in RegLang.languages]DFAofRE [in RegLang.regexp]
DFAtoDFA2 [in RegLang.two_way]
DFA2 [in RegLang.two_way]
DFA2toAFA [in RegLang.shepherdson]
F
FA [in RegLang.dfa]FA.CutOff [in RegLang.dfa]
FA.DFAOps [in RegLang.dfa]
FA.DFA_Acceptance [in RegLang.dfa]
FA.Emptyness [in RegLang.dfa]
Functional [in RegLang.misc]
H
HomDef [in RegLang.languages]I
Image [in RegLang.regexp]K
KleeneAlgorithm [in RegLang.regexp]L
Language [in RegLang.wmso]LeftQuotient [in RegLang.dfa]
M
Minimization [in RegLang.minimization]Minimization.Collapse [in RegLang.minimization]
Minimization.Isomopism [in RegLang.minimization]
Minimization.Prune [in RegLang.minimization]
N
NFA [in RegLang.nfa]NFAtoMSO [in RegLang.wmso]
NFA.Embed [in RegLang.nfa]
NFA.eNFAOps [in RegLang.nfa]
NFA.EpsilonNFA [in RegLang.nfa]
NFA.NFARun [in RegLang.nfa]
NFA.PowersetConstruction [in RegLang.nfa]
NFA2 [in RegLang.two_way]
NFA2toAFA [in RegLang.shepherdson]
NFA2toAFA.CompositeWord [in RegLang.shepherdson]
NonRegular [in RegLang.dfa]
P
Preimage [in RegLang.dfa]Pumping [in RegLang.dfa]
R
RegExp [in RegLang.regexp]RightQuotient [in RegLang.dfa]
V
Vardi [in RegLang.vardi]Vardi.Completeness [in RegLang.vardi]
Abbreviation Index
C
classes_of [in RegLang.myhill_nerode]D
dfa [in RegLang.minimization]R
rank [in RegLang.wmso]V
val [in RegLang.wmso]vec [in RegLang.wmso]
W
word [in RegLang.dfa]word [in RegLang.minimization]
word [in RegLang.myhill_nerode]
word [in RegLang.nfa]
Definition Index
A
accE [in RegLang.dfa]accept [in RegLang.wmso]
agree [in RegLang.wmso]
All [in RegLang.wmso]
All1 [in RegLang.wmso]
And [in RegLang.wmso]
atom [in RegLang.languages]
B
bound [in RegLang.wmso]bsimp [in RegLang.vardi]
C
cat [in RegLang.wmso]cf_lang_eq [in RegLang.myhill_nerode]
classifier_to_dfa [in RegLang.myhill_nerode]
coll [in RegLang.minimization]
collapse [in RegLang.minimization]
collapsed [in RegLang.minimization]
collapse_state [in RegLang.minimization]
collb [in RegLang.minimization]
coll_fun [in RegLang.minimization]
comp [in RegLang.vardi]
compL [in RegLang.vardi]
compl [in RegLang.languages]
compR [in RegLang.vardi]
conc [in RegLang.languages]
connected [in RegLang.minimization]
connectedb [in RegLang.minimization]
cons [in RegLang.wmso]
cr [in RegLang.misc]
D
delta [in RegLang.dfa]delta_s [in RegLang.dfa]
dfa_quot [in RegLang.dfa]
dfa_preim [in RegLang.dfa]
dfa_incl [in RegLang.dfa]
dfa_equiv [in RegLang.dfa]
dfa_empty [in RegLang.dfa]
dfa_inhab [in RegLang.dfa]
dfa_op [in RegLang.dfa]
dfa_compl [in RegLang.dfa]
dfa_void [in RegLang.dfa]
dfa_lang [in RegLang.dfa]
dfa_accept [in RegLang.dfa]
dfa_prune [in RegLang.minimization]
dfa_iso [in RegLang.minimization]
dfa_to_re [in RegLang.regexp]
dfa_to_mg [in RegLang.myhill_nerode]
dfa_to_cf [in RegLang.myhill_nerode]
dfa_to_nfa [in RegLang.nfa]
dfa0 [in RegLang.dfa]
dfa2_of_dfa [in RegLang.two_way]
dfa2_lang [in RegLang.two_way]
dfa2_to_myhill [in RegLang.shepherdson]
dir [in RegLang.two_way]
dlang [in RegLang.languages]
E
edges [in RegLang.regexp]edgesP [in RegLang.regexp]
empty [in RegLang.wmso]
enfa_for_ltn [in RegLang.wmso]
enfa_star [in RegLang.nfa]
enfa_conc [in RegLang.nfa]
enfa_lang [in RegLang.nfa]
eps [in RegLang.languages]
eps_reach [in RegLang.nfa]
exn [in RegLang.wmso]
exseqb [in RegLang.dfa]
Ex1 [in RegLang.wmso]
F
form_of [in RegLang.wmso]functional [in RegLang.misc]
G
glue [in RegLang.wmso]H
homomorphism [in RegLang.languages]I
Iff [in RegLang.wmso]iffT_RL [in RegLang.misc]
iffT_LR [in RegLang.misc]
image [in RegLang.languages]
image_fun [in RegLang.dfa]
image_type [in RegLang.dfa]
imfun_of_surj [in RegLang.myhill_nerode]
imfun_of [in RegLang.myhill_nerode]
init [in RegLang.wmso]
Inter [in RegLang.regexp]
iso [in RegLang.minimization]
iso_inv [in RegLang.minimization]
I_of [in RegLang.wmso]
L
L [in RegLang.two_way]L [in RegLang.regexp]
Lab [in RegLang.dfa]
lang [in RegLang.languages]
Leq [in RegLang.wmso]
leqRW [in RegLang.setoid_leq]
lim [in RegLang.wmso]
M
max [in RegLang.wmso]mg_eq [in RegLang.myhill_nerode]
mg_to_dfa [in RegLang.myhill_nerode]
mg_to_classifier [in RegLang.myhill_nerode]
minimal [in RegLang.minimization]
minimal_classifier [in RegLang.myhill_nerode]
minimize [in RegLang.minimization]
mso_lang [in RegLang.wmso]
N
Neg [in RegLang.regexp]nerode [in RegLang.myhill_nerode]
nfa_of_form [in RegLang.wmso]
nfa_for_ex [in RegLang.wmso]
nfa_for_ltn [in RegLang.wmso]
nfa_for_incl [in RegLang.wmso]
nfa_for_imp [in RegLang.wmso]
nfa_for_bot [in RegLang.wmso]
nfa_of [in RegLang.vardi]
nfa_inhab [in RegLang.nfa]
nfa_star [in RegLang.nfa]
nfa_conc [in RegLang.nfa]
nfa_eps [in RegLang.nfa]
nfa_plus [in RegLang.nfa]
nfa_char [in RegLang.nfa]
nfa_to_dfa [in RegLang.nfa]
nfa_of [in RegLang.nfa]
nfa_lang [in RegLang.nfa]
nfa_accept [in RegLang.nfa]
nfa2_of_dfa [in RegLang.two_way]
nfa2_lang [in RegLang.two_way]
nfa2_config [in RegLang.two_way]
nfa2_to_classifier [in RegLang.shepherdson]
Not [in RegLang.wmso]
O
Or [in RegLang.wmso]ord1 [in RegLang.misc]
P
part [in RegLang.wmso]plus [in RegLang.languages]
pos [in RegLang.two_way]
preimage [in RegLang.languages]
prj0 [in RegLang.wmso]
prod [in RegLang.languages]
pump_Lab [in RegLang.dfa]
Q
quotL [in RegLang.dfa]quotR [in RegLang.dfa]
R
R [in RegLang.two_way]R [in RegLang.regexp]
reachable [in RegLang.minimization]
reachable_s [in RegLang.minimization]
reachable_trans [in RegLang.minimization]
reachable_type [in RegLang.minimization]
read [in RegLang.two_way]
refines [in RegLang.myhill_nerode]
regexp_eqMixin [in RegLang.regexp]
regular [in RegLang.dfa]
reject_cert [in RegLang.vardi]
rep [in RegLang.dfa]
residual [in RegLang.dfa]
residual [in RegLang.languages]
Rev [in RegLang.regexp]
re_image [in RegLang.regexp]
re_equiv [in RegLang.regexp]
re_to_dfa [in RegLang.regexp]
re_to_nfa [in RegLang.regexp]
re_size [in RegLang.regexp]
re_lang [in RegLang.regexp]
right_congruent [in RegLang.myhill_nerode]
run [in RegLang.wmso]
run_table [in RegLang.vardi]
R_size_rec [in RegLang.regexp]
R0 [in RegLang.regexp]
S
satisfies [in RegLang.wmso]single [in RegLang.wmso]
srel [in RegLang.shepherdson]
star [in RegLang.languages]
step [in RegLang.two_way]
String [in RegLang.regexp]
sub [in RegLang.dfa]
succ [in RegLang.wmso]
surjective [in RegLang.misc]
T
Tab [in RegLang.shepherdson]table [in RegLang.shepherdson]
Tab' [in RegLang.shepherdson]
tape [in RegLang.two_way]
terminal [in RegLang.misc]
trans_b0 [in RegLang.wmso]
TT [in RegLang.wmso]
V
valuation [in RegLang.wmso]vec_of_val [in RegLang.wmso]
vec_lang [in RegLang.wmso]
vec_of [in RegLang.wmso]
void [in RegLang.languages]
W
word [in RegLang.languages]Z
zero [in RegLang.wmso]zero_at [in RegLang.wmso]
Record Index
C
classifier [in RegLang.myhill_nerode]classifier_for [in RegLang.myhill_nerode]
D
deterministic [in RegLang.two_way]dfa [in RegLang.dfa]
dfa2 [in RegLang.two_way]
E
enfa [in RegLang.nfa]M
mgClassifier [in RegLang.myhill_nerode]N
nfa [in RegLang.nfa]nfa2 [in RegLang.two_way]
| 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 | (758 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 | (17 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 | (103 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 | (12 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 | (324 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 | (24 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 | (7 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 | (30 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 | (42 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 | (9 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 | (181 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |