| 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 | (2159 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) |
| Binder 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 | (1392 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 | (323 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) |
| 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) |
| 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) |
| 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 | (191 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 [constructor, in RegLang.regexp]
atom [definition, in RegLang.languages]
aT:151 [binder, in RegLang.misc]
aT:157 [binder, in RegLang.misc]
A_start_cat [lemma, in RegLang.dfa]
A1:101 [binder, in RegLang.dfa]
A1:103 [binder, in RegLang.dfa]
A1:107 [binder, in RegLang.dfa]
A1:12 [binder, in RegLang.minimization]
A1:99 [binder, in RegLang.dfa]
A2:100 [binder, in RegLang.dfa]
A2:102 [binder, in RegLang.dfa]
A2:104 [binder, in RegLang.dfa]
A2:108 [binder, in RegLang.dfa]
A2:13 [binder, in RegLang.minimization]
a:1 [binder, in RegLang.setoid_leq]
A:10 [binder, in RegLang.minimization]
a:105 [binder, in RegLang.dfa]
A:107 [binder, in RegLang.wmso]
A:111 [binder, in RegLang.wmso]
A:113 [binder, in RegLang.dfa]
a:115 [binder, in RegLang.dfa]
A:116 [binder, in RegLang.dfa]
a:116 [binder, in RegLang.regexp]
a:120 [binder, in RegLang.regexp]
a:121 [binder, in RegLang.regexp]
a:123 [binder, in RegLang.nfa]
a:127 [binder, in RegLang.regexp]
a:128 [binder, in RegLang.regexp]
A:128 [binder, in RegLang.shepherdson]
A:129 [binder, in RegLang.shepherdson]
a:13 [binder, in RegLang.dfa]
A:13 [binder, in RegLang.nfa]
A:151 [binder, in RegLang.shepherdson]
A:152 [binder, in RegLang.shepherdson]
a:16 [binder, in RegLang.minimization]
a:160 [binder, in RegLang.dfa]
a:161 [binder, in RegLang.dfa]
A:163 [binder, in RegLang.wmso]
a:170 [binder, in RegLang.regexp]
a:18 [binder, in RegLang.languages]
A:2 [binder, in RegLang.minimization]
A:201 [binder, in RegLang.dfa]
A:205 [binder, in RegLang.dfa]
a:225 [binder, in RegLang.dfa]
a:226 [binder, in RegLang.dfa]
a:24 [binder, in RegLang.dfa]
a:26 [binder, in RegLang.nfa]
A:28 [binder, in RegLang.dfa]
a:28 [binder, in RegLang.vardi]
A:29 [binder, in RegLang.minimization]
a:31 [binder, in RegLang.myhill_nerode]
a:33 [binder, in RegLang.dfa]
a:33 [binder, in RegLang.two_way]
a:333 [binder, in RegLang.wmso]
a:34 [binder, in RegLang.misc]
a:354 [binder, in RegLang.wmso]
a:37 [binder, in RegLang.minimization]
a:39 [binder, in RegLang.minimization]
a:4 [binder, in RegLang.wmso]
a:41 [binder, in RegLang.dfa]
a:41 [binder, in RegLang.nfa]
a:43 [binder, in RegLang.misc]
a:43 [binder, in RegLang.wmso]
A:44 [binder, in RegLang.two_way]
a:45 [binder, in RegLang.dfa]
a:46 [binder, in RegLang.wmso]
a:49 [binder, in RegLang.misc]
a:49 [binder, in RegLang.minimization]
a:49 [binder, in RegLang.wmso]
a:5 [binder, in RegLang.setoid_leq]
a:52 [binder, in RegLang.nfa]
a:56 [binder, in RegLang.two_way]
a:56 [binder, in RegLang.minimization]
a:57 [binder, in RegLang.dfa]
a:58 [binder, in RegLang.dfa]
a:58 [binder, in RegLang.nfa]
a:59 [binder, in RegLang.dfa]
a:59 [binder, in RegLang.misc]
A:59 [binder, in RegLang.wmso]
A:6 [binder, in RegLang.minimization]
a:60 [binder, in RegLang.nfa]
a:60 [binder, in RegLang.minimization]
a:62 [binder, in RegLang.dfa]
a:63 [binder, in RegLang.dfa]
a:64 [binder, in RegLang.nfa]
A:65 [binder, in RegLang.minimization]
A:66 [binder, in RegLang.minimization]
A:67 [binder, in RegLang.minimization]
a:68 [binder, in RegLang.nfa]
A:68 [binder, in RegLang.minimization]
a:69 [binder, in RegLang.dfa]
A:69 [binder, in RegLang.minimization]
A:7 [binder, in RegLang.nfa]
A:7 [binder, in RegLang.minimization]
A:70 [binder, in RegLang.minimization]
A:71 [binder, in RegLang.minimization]
A:72 [binder, in RegLang.minimization]
A:73 [binder, in RegLang.minimization]
A:74 [binder, in RegLang.minimization]
A:75 [binder, in RegLang.minimization]
A:76 [binder, in RegLang.minimization]
a:77 [binder, in RegLang.regexp]
A:77 [binder, in RegLang.minimization]
a:78 [binder, in RegLang.regexp]
a:80 [binder, in RegLang.nfa]
A:83 [binder, in RegLang.wmso]
a:87 [binder, in RegLang.dfa]
A:88 [binder, in RegLang.wmso]
a:9 [binder, in RegLang.myhill_nerode]
a:93 [binder, 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]
bs:140 [binder, in RegLang.wmso]
bs:152 [binder, in RegLang.wmso]
bs:99 [binder, in RegLang.wmso]
b1:4 [binder, in RegLang.misc]
b1:56 [binder, in RegLang.misc]
b2:5 [binder, in RegLang.misc]
b2:57 [binder, in RegLang.misc]
b:1 [binder, in RegLang.shepherdson]
b:106 [binder, in RegLang.dfa]
b:108 [binder, in RegLang.wmso]
B:11 [binder, in RegLang.minimization]
b:113 [binder, in RegLang.wmso]
b:115 [binder, in RegLang.wmso]
b:116 [binder, in RegLang.wmso]
b:119 [binder, in RegLang.wmso]
b:124 [binder, in RegLang.wmso]
b:127 [binder, in RegLang.wmso]
b:133 [binder, in RegLang.wmso]
b:147 [binder, in RegLang.shepherdson]
b:2 [binder, in RegLang.setoid_leq]
b:227 [binder, in RegLang.dfa]
B:31 [binder, in RegLang.minimization]
b:46 [binder, in RegLang.misc]
b:47 [binder, in RegLang.misc]
b:6 [binder, in RegLang.setoid_leq]
B:60 [binder, in RegLang.wmso]
b:62 [binder, in RegLang.nfa]
b:62 [binder, in RegLang.misc]
b:63 [binder, in RegLang.misc]
B:78 [binder, in RegLang.minimization]
b:86 [binder, in RegLang.wmso]
b:92 [binder, in RegLang.wmso]
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_nseq_eq [lemma, in RegLang.dfa]
cat_size [lemma, in RegLang.wmso]
cat_beyond [lemma, in RegLang.wmso]
cat_prefix [lemma, in RegLang.wmso]
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]
char':118 [binder, in RegLang.dfa]
char':184 [binder, in RegLang.regexp]
char:10 [binder, in RegLang.regexp]
char:117 [binder, in RegLang.dfa]
char:135 [binder, in RegLang.dfa]
char:14 [binder, in RegLang.regexp]
char:152 [binder, in RegLang.regexp]
char:156 [binder, in RegLang.regexp]
char:159 [binder, in RegLang.regexp]
char:162 [binder, in RegLang.dfa]
char:163 [binder, in RegLang.regexp]
char:165 [binder, in RegLang.regexp]
char:166 [binder, in RegLang.dfa]
char:168 [binder, in RegLang.regexp]
char:169 [binder, in RegLang.dfa]
char:171 [binder, in RegLang.regexp]
char:183 [binder, in RegLang.regexp]
char:187 [binder, in RegLang.regexp]
char:191 [binder, in RegLang.regexp]
char:194 [binder, in RegLang.regexp]
char:218 [binder, in RegLang.wmso]
char:22 [binder, in RegLang.regexp]
char:29 [binder, in RegLang.regexp]
char:34 [binder, in RegLang.regexp]
char:6 [binder, in RegLang.regexp]
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]
cl:58 [binder, in RegLang.shepherdson]
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_equiv [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.languages]
compL [definition, in RegLang.vardi]
compR [definition, in RegLang.vardi]
Conc [constructor, in RegLang.regexp]
conc [definition, in RegLang.languages]
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]
cr [definition, in RegLang.misc]
crK [lemma, in RegLang.misc]
cr:59 [binder, in RegLang.shepherdson]
cs:56 [binder, in RegLang.shepherdson]
c:101 [binder, in RegLang.nfa]
C:13 [binder, in RegLang.vardi]
c:19 [binder, in RegLang.shepherdson]
c:26 [binder, in RegLang.two_way]
c:35 [binder, in RegLang.shepherdson]
c:40 [binder, in RegLang.shepherdson]
c:70 [binder, in RegLang.wmso]
c:83 [binder, in RegLang.shepherdson]
c:84 [binder, in RegLang.nfa]
c:84 [binder, in RegLang.shepherdson]
c:98 [binder, in RegLang.shepherdson]
D
DecidableLanguages [section, in RegLang.languages]DecidableLanguages.char [variable, in RegLang.languages]
decP:173 [binder, in RegLang.misc]
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_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_nfa_correct [lemma, in RegLang.nfa]
dfa_to_nfa [definition, in RegLang.nfa]
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_mg [definition, in RegLang.myhill_nerode]
dfa_to_cf_size [lemma, in RegLang.myhill_nerode]
dfa_to_cf [definition, in RegLang.myhill_nerode]
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]
d:20 [binder, in RegLang.shepherdson]
d:27 [binder, in RegLang.two_way]
d:36 [binder, in RegLang.shepherdson]
d:41 [binder, in RegLang.shepherdson]
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_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]
enfa_for_ltn [definition, in RegLang.wmso]
epiK [lemma, in RegLang.misc]
Eps [constructor, in RegLang.regexp]
eps [definition, in RegLang.languages]
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]
e1:149 [binder, in RegLang.misc]
e1:4 [binder, in RegLang.regexp]
e2:150 [binder, in RegLang.misc]
e2:5 [binder, in RegLang.regexp]
e:112 [binder, in RegLang.misc]
E:12 [binder, in RegLang.myhill_nerode]
e:154 [binder, in RegLang.regexp]
e:177 [binder, in RegLang.regexp]
e:180 [binder, in RegLang.regexp]
e:188 [binder, in RegLang.regexp]
e:192 [binder, in RegLang.regexp]
e:30 [binder, in RegLang.regexp]
E:37 [binder, in RegLang.myhill_nerode]
e:45 [binder, in RegLang.regexp]
e:47 [binder, in RegLang.regexp]
E:6 [binder, in RegLang.myhill_nerode]
e:7 [binder, in RegLang.regexp]
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_eqType [definition, in RegLang.regexp]
form_ofP [lemma, in RegLang.wmso]
form_of [definition, in RegLang.wmso]
functional [definition, in RegLang.misc]
Functional [section, in RegLang.misc]
functional_sub [lemma, in RegLang.misc]
functional_srel [lemma, in RegLang.shepherdson]
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]
f:153 [binder, in RegLang.misc]
f:158 [binder, in RegLang.misc]
f:161 [binder, in RegLang.misc]
f:164 [binder, in RegLang.misc]
f:169 [binder, in RegLang.misc]
F:17 [binder, in RegLang.regexp]
f:176 [binder, in RegLang.dfa]
F:25 [binder, in RegLang.regexp]
F:264 [binder, in RegLang.wmso]
F:269 [binder, in RegLang.wmso]
F:276 [binder, in RegLang.wmso]
f:30 [binder, in RegLang.minimization]
F:36 [binder, in RegLang.regexp]
f:64 [binder, in RegLang.two_way]
f:66 [binder, in RegLang.two_way]
F:67 [binder, in RegLang.misc]
f:92 [binder, in RegLang.misc]
f:95 [binder, in RegLang.misc]
G
glue [definition, in RegLang.wmso]H
Hi:144 [binder, in RegLang.nfa]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]
h:119 [binder, in RegLang.dfa]
H:137 [binder, in RegLang.shepherdson]
h:185 [binder, in RegLang.regexp]
H:26 [binder, in RegLang.myhill_nerode]
H:65 [binder, in RegLang.myhill_nerode]
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 [section, in RegLang.regexp]
image [definition, in RegLang.languages]
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_refines [lemma, in RegLang.shepherdson]
image_rc [lemma, in RegLang.shepherdson]
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_max [lemma, in RegLang.misc]
inord_inj [lemma, in RegLang.shepherdson]
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]
i':12 [binder, in RegLang.two_way]
I':23 [binder, in RegLang.wmso]
I':28 [binder, in RegLang.wmso]
I':30 [binder, in RegLang.wmso]
I':34 [binder, in RegLang.wmso]
i:10 [binder, in RegLang.vardi]
i:106 [binder, in RegLang.shepherdson]
i:11 [binder, in RegLang.regexp]
i:11 [binder, in RegLang.two_way]
I:11 [binder, in RegLang.wmso]
i:115 [binder, in RegLang.shepherdson]
i:119 [binder, in RegLang.misc]
i:12 [binder, in RegLang.regexp]
i:120 [binder, in RegLang.misc]
i:123 [binder, in RegLang.wmso]
i:13 [binder, in RegLang.shepherdson]
i:130 [binder, in RegLang.wmso]
i:132 [binder, in RegLang.wmso]
i:14 [binder, in RegLang.minimization]
i:14 [binder, in RegLang.vardi]
i:141 [binder, in RegLang.wmso]
i:143 [binder, in RegLang.nfa]
i:143 [binder, in RegLang.wmso]
i:148 [binder, in RegLang.nfa]
i:159 [binder, in RegLang.wmso]
i:160 [binder, in RegLang.wmso]
i:18 [binder, in RegLang.regexp]
i:194 [binder, in RegLang.dfa]
i:194 [binder, in RegLang.wmso]
i:195 [binder, in RegLang.wmso]
i:196 [binder, in RegLang.wmso]
I:200 [binder, in RegLang.wmso]
i:204 [binder, in RegLang.dfa]
I:204 [binder, in RegLang.wmso]
i:206 [binder, in RegLang.wmso]
I:208 [binder, in RegLang.wmso]
I:210 [binder, in RegLang.wmso]
i:212 [binder, in RegLang.dfa]
I:212 [binder, in RegLang.wmso]
i:213 [binder, in RegLang.dfa]
I:215 [binder, in RegLang.wmso]
I:22 [binder, in RegLang.wmso]
I:220 [binder, in RegLang.wmso]
i:222 [binder, in RegLang.dfa]
I:223 [binder, in RegLang.wmso]
I:225 [binder, in RegLang.wmso]
I:228 [binder, in RegLang.wmso]
I:230 [binder, in RegLang.wmso]
I:233 [binder, in RegLang.wmso]
I:238 [binder, in RegLang.wmso]
I:244 [binder, in RegLang.wmso]
I:248 [binder, in RegLang.wmso]
I:250 [binder, in RegLang.wmso]
I:254 [binder, in RegLang.wmso]
i:257 [binder, in RegLang.wmso]
i:258 [binder, in RegLang.wmso]
i:259 [binder, in RegLang.wmso]
i:26 [binder, in RegLang.regexp]
i:260 [binder, in RegLang.wmso]
I:265 [binder, in RegLang.wmso]
i:266 [binder, in RegLang.wmso]
i:27 [binder, in RegLang.regexp]
I:27 [binder, in RegLang.wmso]
I:270 [binder, in RegLang.wmso]
i:273 [binder, in RegLang.wmso]
I:277 [binder, in RegLang.wmso]
i:278 [binder, in RegLang.wmso]
i:28 [binder, in RegLang.regexp]
I:281 [binder, in RegLang.wmso]
I:285 [binder, in RegLang.wmso]
I:29 [binder, in RegLang.wmso]
I:293 [binder, in RegLang.wmso]
I:299 [binder, in RegLang.wmso]
i:30 [binder, in RegLang.shepherdson]
I:303 [binder, in RegLang.wmso]
I:309 [binder, in RegLang.wmso]
I:311 [binder, in RegLang.wmso]
I:315 [binder, in RegLang.wmso]
I:319 [binder, in RegLang.wmso]
I:326 [binder, in RegLang.wmso]
I:33 [binder, in RegLang.wmso]
i:34 [binder, in RegLang.vardi]
I:341 [binder, in RegLang.wmso]
i:35 [binder, in RegLang.languages]
I:351 [binder, in RegLang.wmso]
I:358 [binder, in RegLang.wmso]
i:36 [binder, in RegLang.vardi]
I:365 [binder, in RegLang.wmso]
i:369 [binder, in RegLang.wmso]
i:37 [binder, in RegLang.vardi]
i:371 [binder, in RegLang.wmso]
i:374 [binder, in RegLang.wmso]
i:375 [binder, in RegLang.wmso]
i:377 [binder, in RegLang.wmso]
i:38 [binder, in RegLang.regexp]
i:38 [binder, in RegLang.vardi]
i:39 [binder, in RegLang.regexp]
i:41 [binder, in RegLang.wmso]
i:46 [binder, in RegLang.shepherdson]
i:5 [binder, in RegLang.two_way]
i:5 [binder, in RegLang.vardi]
i:52 [binder, in RegLang.shepherdson]
i:58 [binder, in RegLang.regexp]
i:59 [binder, in RegLang.two_way]
i:63 [binder, in RegLang.two_way]
i:63 [binder, in RegLang.shepherdson]
i:66 [binder, in RegLang.regexp]
i:67 [binder, in RegLang.two_way]
i:70 [binder, in RegLang.misc]
i:73 [binder, in RegLang.misc]
i:75 [binder, in RegLang.dfa]
i:75 [binder, in RegLang.shepherdson]
i:79 [binder, in RegLang.shepherdson]
I:8 [binder, in RegLang.wmso]
i:8 [binder, in RegLang.shepherdson]
i:82 [binder, in RegLang.dfa]
i:86 [binder, in RegLang.regexp]
i:87 [binder, in RegLang.regexp]
i:88 [binder, in RegLang.regexp]
J
j:107 [binder, in RegLang.shepherdson]j:116 [binder, in RegLang.shepherdson]
j:14 [binder, in RegLang.shepherdson]
j:195 [binder, in RegLang.dfa]
j:32 [binder, in RegLang.shepherdson]
j:35 [binder, in RegLang.vardi]
j:47 [binder, in RegLang.shepherdson]
j:48 [binder, in RegLang.two_way]
j:53 [binder, in RegLang.shepherdson]
j:64 [binder, in RegLang.shepherdson]
j:7 [binder, in RegLang.vardi]
j:76 [binder, in RegLang.dfa]
j:76 [binder, in RegLang.shepherdson]
j:80 [binder, in RegLang.shepherdson]
j:9 [binder, in RegLang.shepherdson]
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]
k':100 [binder, in RegLang.shepherdson]
k':37 [binder, in RegLang.shepherdson]
k':50 [binder, in RegLang.shepherdson]
k':61 [binder, in RegLang.shepherdson]
k':92 [binder, in RegLang.shepherdson]
k:108 [binder, in RegLang.shepherdson]
k:117 [binder, in RegLang.shepherdson]
k:122 [binder, in RegLang.wmso]
k:131 [binder, in RegLang.wmso]
k:132 [binder, in RegLang.shepherdson]
k:134 [binder, in RegLang.shepherdson]
k:136 [binder, in RegLang.wmso]
k:142 [binder, in RegLang.wmso]
k:144 [binder, in RegLang.wmso]
k:145 [binder, in RegLang.wmso]
k:146 [binder, in RegLang.wmso]
k:147 [binder, in RegLang.wmso]
k:151 [binder, in RegLang.wmso]
k:155 [binder, in RegLang.wmso]
k:17 [binder, in RegLang.shepherdson]
k:189 [binder, in RegLang.wmso]
k:21 [binder, in RegLang.shepherdson]
k:215 [binder, in RegLang.dfa]
k:27 [binder, in RegLang.shepherdson]
k:290 [binder, in RegLang.wmso]
k:33 [binder, in RegLang.shepherdson]
k:342 [binder, in RegLang.wmso]
k:352 [binder, in RegLang.wmso]
k:38 [binder, in RegLang.shepherdson]
k:42 [binder, in RegLang.shepherdson]
k:45 [binder, in RegLang.wmso]
k:48 [binder, in RegLang.wmso]
k:49 [binder, in RegLang.shepherdson]
k:60 [binder, in RegLang.shepherdson]
k:68 [binder, in RegLang.misc]
k:72 [binder, in RegLang.shepherdson]
k:89 [binder, in RegLang.shepherdson]
k:9 [binder, in RegLang.wmso]
k:91 [binder, in RegLang.shepherdson]
k:96 [binder, in RegLang.shepherdson]
L
L [definition, in RegLang.regexp]L [definition, in RegLang.two_way]
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]
L1:136 [binder, in RegLang.dfa]
L1:163 [binder, in RegLang.dfa]
L1:20 [binder, in RegLang.myhill_nerode]
L1:23 [binder, in RegLang.languages]
L1:23 [binder, in RegLang.myhill_nerode]
L1:26 [binder, in RegLang.languages]
L1:30 [binder, in RegLang.dfa]
L1:32 [binder, in RegLang.languages]
L1:43 [binder, in RegLang.languages]
L1:47 [binder, in RegLang.dfa]
L1:50 [binder, in RegLang.dfa]
L1:50 [binder, in RegLang.languages]
l1:52 [binder, in RegLang.languages]
L1:59 [binder, in RegLang.myhill_nerode]
L1:62 [binder, in RegLang.myhill_nerode]
l1:66 [binder, in RegLang.languages]
L1:8 [binder, in RegLang.languages]
L2:137 [binder, in RegLang.dfa]
L2:164 [binder, in RegLang.dfa]
L2:21 [binder, in RegLang.myhill_nerode]
L2:24 [binder, in RegLang.languages]
L2:24 [binder, in RegLang.myhill_nerode]
L2:27 [binder, in RegLang.languages]
L2:31 [binder, in RegLang.dfa]
L2:33 [binder, in RegLang.languages]
L2:44 [binder, in RegLang.languages]
L2:48 [binder, in RegLang.dfa]
L2:51 [binder, in RegLang.dfa]
L2:51 [binder, in RegLang.languages]
l2:53 [binder, in RegLang.languages]
L2:60 [binder, in RegLang.myhill_nerode]
L2:63 [binder, in RegLang.myhill_nerode]
l2:67 [binder, in RegLang.languages]
L2:9 [binder, in RegLang.languages]
l3:54 [binder, in RegLang.languages]
l4:55 [binder, in RegLang.languages]
L:11 [binder, in RegLang.myhill_nerode]
L:12 [binder, in RegLang.languages]
L:120 [binder, in RegLang.dfa]
L:15 [binder, in RegLang.myhill_nerode]
L:152 [binder, in RegLang.nfa]
L:153 [binder, in RegLang.regexp]
L:167 [binder, in RegLang.dfa]
L:173 [binder, in RegLang.dfa]
L:177 [binder, in RegLang.dfa]
L:186 [binder, in RegLang.regexp]
L:195 [binder, in RegLang.regexp]
L:214 [binder, in RegLang.dfa]
L:22 [binder, in RegLang.languages]
L:27 [binder, in RegLang.dfa]
L:30 [binder, in RegLang.languages]
L:33 [binder, in RegLang.myhill_nerode]
L:36 [binder, in RegLang.languages]
L:36 [binder, in RegLang.myhill_nerode]
L:41 [binder, in RegLang.myhill_nerode]
L:45 [binder, in RegLang.myhill_nerode]
L:47 [binder, in RegLang.myhill_nerode]
L:49 [binder, in RegLang.myhill_nerode]
L:5 [binder, in RegLang.languages]
L:51 [binder, in RegLang.myhill_nerode]
L:53 [binder, in RegLang.myhill_nerode]
L:54 [binder, in RegLang.dfa]
L:55 [binder, in RegLang.myhill_nerode]
L:56 [binder, in RegLang.languages]
L:57 [binder, in RegLang.myhill_nerode]
L:62 [binder, in RegLang.languages]
L:63 [binder, in RegLang.languages]
M
max [definition, in RegLang.wmso]max_mem [lemma, in RegLang.misc]
measure:15 [binder, in RegLang.misc]
mem_R0 [lemma, in RegLang.regexp]
mem_I_of [lemma, in RegLang.wmso]
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]
min_subFinType [definition, in RegLang.minimization]
min_finType [definition, in RegLang.minimization]
min_choiceType [definition, in RegLang.minimization]
min_eqType [definition, in RegLang.minimization]
min_subType [definition, in RegLang.minimization]
min_quotType [definition, 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]
M1:22 [binder, in RegLang.myhill_nerode]
M1:25 [binder, in RegLang.myhill_nerode]
m:117 [binder, in RegLang.misc]
m:2 [binder, in RegLang.two_way]
m:26 [binder, in RegLang.wmso]
m:28 [binder, in RegLang.misc]
M:30 [binder, in RegLang.two_way]
m:32 [binder, in RegLang.misc]
m:335 [binder, in RegLang.wmso]
M:34 [binder, in RegLang.myhill_nerode]
m:350 [binder, in RegLang.wmso]
m:364 [binder, in RegLang.wmso]
m:37 [binder, in RegLang.regexp]
m:4 [binder, in RegLang.shepherdson]
m:48 [binder, in RegLang.shepherdson]
M:58 [binder, in RegLang.myhill_nerode]
M:66 [binder, in RegLang.nfa]
m:69 [binder, in RegLang.misc]
m:7 [binder, in RegLang.two_way]
m:7 [binder, in RegLang.setoid_leq]
M:78 [binder, in RegLang.nfa]
m:90 [binder, in RegLang.shepherdson]
m:95 [binder, in RegLang.shepherdson]
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_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_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.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]
Ns:308 [binder, in RegLang.wmso]
Ns:313 [binder, in RegLang.wmso]
Ns:317 [binder, in RegLang.wmso]
Ns:321 [binder, in RegLang.wmso]
Ns:327 [binder, in RegLang.wmso]
Ns:349 [binder, in RegLang.wmso]
Ns:357 [binder, in RegLang.wmso]
Ns:363 [binder, in RegLang.wmso]
nth_cons [lemma, in RegLang.misc]
nth_glueS [lemma, in RegLang.wmso]
nth_glue0 [lemma, in RegLang.wmso]
n0:71 [binder, in RegLang.misc]
n1:178 [binder, in RegLang.dfa]
n1:186 [binder, in RegLang.dfa]
n1:188 [binder, in RegLang.dfa]
n1:190 [binder, in RegLang.dfa]
n1:223 [binder, in RegLang.dfa]
N1:61 [binder, in RegLang.myhill_nerode]
N1:64 [binder, in RegLang.myhill_nerode]
n2:179 [binder, in RegLang.dfa]
n2:187 [binder, in RegLang.dfa]
n2:189 [binder, in RegLang.dfa]
n2:191 [binder, in RegLang.dfa]
n2:224 [binder, in RegLang.dfa]
n:1 [binder, in RegLang.two_way]
n:10 [binder, in RegLang.two_way]
n:100 [binder, in RegLang.misc]
n:100 [binder, in RegLang.wmso]
n:101 [binder, in RegLang.misc]
n:102 [binder, in RegLang.misc]
n:106 [binder, in RegLang.wmso]
n:110 [binder, in RegLang.wmso]
n:117 [binder, in RegLang.wmso]
n:118 [binder, in RegLang.misc]
n:120 [binder, in RegLang.wmso]
n:121 [binder, in RegLang.misc]
n:122 [binder, in RegLang.misc]
n:123 [binder, in RegLang.misc]
n:124 [binder, in RegLang.misc]
n:125 [binder, in RegLang.wmso]
n:128 [binder, in RegLang.wmso]
n:134 [binder, in RegLang.wmso]
n:138 [binder, in RegLang.wmso]
n:145 [binder, in RegLang.regexp]
n:149 [binder, in RegLang.regexp]
N:149 [binder, in RegLang.nfa]
n:149 [binder, in RegLang.wmso]
n:150 [binder, in RegLang.regexp]
N:150 [binder, in RegLang.nfa]
N:153 [binder, in RegLang.nfa]
n:153 [binder, in RegLang.wmso]
n:157 [binder, in RegLang.wmso]
n:161 [binder, in RegLang.wmso]
n:168 [binder, in RegLang.wmso]
N:17 [binder, in RegLang.wmso]
n:173 [binder, in RegLang.wmso]
n:178 [binder, in RegLang.wmso]
n:180 [binder, in RegLang.dfa]
n:185 [binder, in RegLang.dfa]
n:186 [binder, in RegLang.wmso]
n:192 [binder, in RegLang.dfa]
n:192 [binder, in RegLang.wmso]
n:197 [binder, in RegLang.wmso]
n:199 [binder, in RegLang.dfa]
n:2 [binder, in RegLang.wmso]
n:201 [binder, in RegLang.wmso]
n:203 [binder, in RegLang.wmso]
n:205 [binder, in RegLang.wmso]
n:209 [binder, in RegLang.wmso]
n:21 [binder, in RegLang.wmso]
n:216 [binder, in RegLang.wmso]
n:24 [binder, in RegLang.misc]
N:246 [binder, in RegLang.wmso]
n:25 [binder, in RegLang.two_way]
n:25 [binder, in RegLang.wmso]
n:252 [binder, in RegLang.wmso]
n:256 [binder, in RegLang.wmso]
n:27 [binder, in RegLang.misc]
n:283 [binder, in RegLang.wmso]
n:287 [binder, in RegLang.wmso]
n:3 [binder, in RegLang.shepherdson]
n:31 [binder, in RegLang.misc]
n:312 [binder, in RegLang.wmso]
n:316 [binder, in RegLang.wmso]
n:320 [binder, in RegLang.wmso]
n:322 [binder, in RegLang.wmso]
n:324 [binder, in RegLang.wmso]
n:343 [binder, in RegLang.wmso]
n:35 [binder, in RegLang.misc]
n:370 [binder, in RegLang.wmso]
n:38 [binder, in RegLang.wmso]
N:46 [binder, in RegLang.myhill_nerode]
N:48 [binder, in RegLang.myhill_nerode]
N:50 [binder, in RegLang.myhill_nerode]
n:51 [binder, in RegLang.wmso]
N:52 [binder, in RegLang.myhill_nerode]
N:54 [binder, in RegLang.myhill_nerode]
N:56 [binder, in RegLang.myhill_nerode]
n:57 [binder, in RegLang.wmso]
n:58 [binder, in RegLang.wmso]
n:6 [binder, in RegLang.two_way]
n:61 [binder, in RegLang.wmso]
N:65 [binder, in RegLang.nfa]
n:67 [binder, in RegLang.wmso]
N:7 [binder, in RegLang.wmso]
n:76 [binder, in RegLang.wmso]
N:77 [binder, in RegLang.nfa]
n:78 [binder, in RegLang.dfa]
n:79 [binder, in RegLang.wmso]
n:8 [binder, in RegLang.two_way]
n:8 [binder, in RegLang.setoid_leq]
n:82 [binder, in RegLang.wmso]
n:87 [binder, in RegLang.wmso]
n:9 [binder, in RegLang.two_way]
n:95 [binder, in RegLang.wmso]
n:99 [binder, 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]
o:113 [binder, in RegLang.nfa]
P
paq:347 [binder, in RegLang.wmso]part [definition, in RegLang.wmso]
Plus [constructor, in RegLang.regexp]
plus [definition, in RegLang.languages]
plusP [lemma, in RegLang.languages]
pos [definition, in RegLang.two_way]
pq:26 [binder, in RegLang.shepherdson]
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]
Px:109 [binder, in RegLang.misc]
Py:110 [binder, in RegLang.misc]
p':43 [binder, in RegLang.nfa]
p':57 [binder, in RegLang.shepherdson]
p':67 [binder, in RegLang.shepherdson]
p':68 [binder, in RegLang.shepherdson]
p':94 [binder, in RegLang.shepherdson]
P1:86 [binder, in RegLang.misc]
P2:87 [binder, in RegLang.misc]
p:102 [binder, in RegLang.nfa]
p:104 [binder, in RegLang.shepherdson]
P:105 [binder, in RegLang.misc]
p:109 [binder, in RegLang.nfa]
p:111 [binder, in RegLang.nfa]
p:113 [binder, in RegLang.shepherdson]
p:116 [binder, in RegLang.misc]
p:12 [binder, in RegLang.dfa]
p:122 [binder, in RegLang.nfa]
p:124 [binder, in RegLang.nfa]
p:129 [binder, in RegLang.nfa]
p:13 [binder, in RegLang.two_way]
p:133 [binder, in RegLang.nfa]
p:138 [binder, in RegLang.nfa]
p:139 [binder, in RegLang.shepherdson]
p:141 [binder, in RegLang.nfa]
p:142 [binder, in RegLang.shepherdson]
p:149 [binder, in RegLang.shepherdson]
p:15 [binder, in RegLang.dfa]
p:16 [binder, in RegLang.misc]
P:170 [binder, in RegLang.dfa]
P:171 [binder, in RegLang.dfa]
P:172 [binder, in RegLang.misc]
p:18 [binder, in RegLang.dfa]
P:2 [binder, in RegLang.misc]
P:2 [binder, in RegLang.shepherdson]
p:202 [binder, in RegLang.dfa]
p:21 [binder, in RegLang.vardi]
p:22 [binder, in RegLang.dfa]
P:23 [binder, in RegLang.regexp]
p:23 [binder, in RegLang.vardi]
p:25 [binder, in RegLang.nfa]
p:25 [binder, in RegLang.vardi]
p:29 [binder, in RegLang.nfa]
p:29 [binder, in RegLang.shepherdson]
p:32 [binder, in RegLang.two_way]
p:35 [binder, in RegLang.nfa]
p:35 [binder, in RegLang.two_way]
p:353 [binder, in RegLang.wmso]
p:37 [binder, in RegLang.nfa]
p:37 [binder, in RegLang.two_way]
p:40 [binder, in RegLang.nfa]
p:42 [binder, in RegLang.minimization]
p:44 [binder, in RegLang.nfa]
p:44 [binder, in RegLang.shepherdson]
P:45 [binder, in RegLang.misc]
p:45 [binder, in RegLang.minimization]
p:46 [binder, in RegLang.nfa]
p:47 [binder, in RegLang.two_way]
p:50 [binder, in RegLang.minimization]
P:51 [binder, in RegLang.misc]
p:52 [binder, in RegLang.minimization]
p:53 [binder, in RegLang.minimization]
p:54 [binder, in RegLang.nfa]
p:54 [binder, in RegLang.shepherdson]
p:55 [binder, in RegLang.regexp]
p:6 [binder, in RegLang.vardi]
p:61 [binder, in RegLang.nfa]
P:61 [binder, in RegLang.misc]
p:63 [binder, in RegLang.regexp]
p:64 [binder, in RegLang.wmso]
p:65 [binder, in RegLang.shepherdson]
P:66 [binder, in RegLang.misc]
p:67 [binder, in RegLang.nfa]
p:71 [binder, in RegLang.wmso]
p:71 [binder, in RegLang.shepherdson]
p:74 [binder, in RegLang.regexp]
p:77 [binder, in RegLang.dfa]
p:77 [binder, in RegLang.shepherdson]
p:79 [binder, in RegLang.nfa]
p:79 [binder, in RegLang.misc]
p:8 [binder, in RegLang.dfa]
p:80 [binder, in RegLang.dfa]
p:80 [binder, in RegLang.regexp]
p:81 [binder, in RegLang.misc]
p:81 [binder, in RegLang.shepherdson]
p:83 [binder, in RegLang.dfa]
p:84 [binder, in RegLang.wmso]
p:85 [binder, in RegLang.dfa]
p:85 [binder, in RegLang.nfa]
p:86 [binder, in RegLang.shepherdson]
p:89 [binder, in RegLang.wmso]
p:90 [binder, in RegLang.nfa]
p:93 [binder, in RegLang.wmso]
p:93 [binder, in RegLang.shepherdson]
p:95 [binder, in RegLang.nfa]
p:97 [binder, in RegLang.nfa]
p:97 [binder, in RegLang.misc]
p:97 [binder, in RegLang.shepherdson]
Q
quotL [definition, in RegLang.dfa]quotR [definition, in RegLang.dfa]
q':339 [binder, in RegLang.wmso]
q:103 [binder, in RegLang.nfa]
q:105 [binder, in RegLang.shepherdson]
q:11 [binder, in RegLang.vardi]
q:114 [binder, in RegLang.wmso]
q:114 [binder, in RegLang.shepherdson]
q:125 [binder, in RegLang.nfa]
q:129 [binder, in RegLang.dfa]
q:133 [binder, in RegLang.dfa]
q:136 [binder, in RegLang.shepherdson]
q:140 [binder, in RegLang.shepherdson]
q:143 [binder, in RegLang.shepherdson]
q:148 [binder, in RegLang.shepherdson]
q:149 [binder, in RegLang.dfa]
q:150 [binder, in RegLang.shepherdson]
q:153 [binder, in RegLang.dfa]
q:156 [binder, in RegLang.dfa]
q:157 [binder, in RegLang.dfa]
q:158 [binder, in RegLang.dfa]
q:22 [binder, in RegLang.vardi]
q:24 [binder, in RegLang.nfa]
q:24 [binder, in RegLang.two_way]
q:24 [binder, in RegLang.vardi]
q:25 [binder, in RegLang.shepherdson]
q:26 [binder, in RegLang.vardi]
q:27 [binder, in RegLang.nfa]
q:28 [binder, in RegLang.two_way]
Q:3 [binder, in RegLang.misc]
q:30 [binder, in RegLang.nfa]
q:31 [binder, in RegLang.shepherdson]
q:33 [binder, in RegLang.minimization]
q:337 [binder, in RegLang.wmso]
q:344 [binder, in RegLang.wmso]
q:355 [binder, in RegLang.wmso]
q:356 [binder, in RegLang.wmso]
q:359 [binder, in RegLang.wmso]
q:36 [binder, in RegLang.nfa]
q:360 [binder, in RegLang.wmso]
q:362 [binder, in RegLang.wmso]
q:366 [binder, in RegLang.wmso]
q:367 [binder, in RegLang.wmso]
q:376 [binder, in RegLang.wmso]
q:38 [binder, in RegLang.nfa]
q:42 [binder, in RegLang.dfa]
q:42 [binder, in RegLang.nfa]
q:43 [binder, in RegLang.minimization]
q:44 [binder, in RegLang.dfa]
q:45 [binder, in RegLang.shepherdson]
q:46 [binder, in RegLang.minimization]
q:47 [binder, in RegLang.nfa]
q:48 [binder, in RegLang.nfa]
q:51 [binder, in RegLang.minimization]
q:53 [binder, in RegLang.nfa]
q:53 [binder, in RegLang.two_way]
q:54 [binder, in RegLang.two_way]
q:54 [binder, in RegLang.minimization]
q:55 [binder, in RegLang.two_way]
q:55 [binder, in RegLang.shepherdson]
q:56 [binder, in RegLang.regexp]
q:57 [binder, in RegLang.two_way]
q:60 [binder, in RegLang.two_way]
q:62 [binder, in RegLang.two_way]
q:63 [binder, in RegLang.nfa]
q:64 [binder, in RegLang.regexp]
q:65 [binder, in RegLang.two_way]
q:66 [binder, in RegLang.wmso]
q:66 [binder, in RegLang.shepherdson]
q:69 [binder, in RegLang.nfa]
q:72 [binder, in RegLang.wmso]
q:73 [binder, in RegLang.nfa]
q:75 [binder, in RegLang.regexp]
q:75 [binder, in RegLang.nfa]
q:78 [binder, in RegLang.shepherdson]
q:8 [binder, in RegLang.vardi]
q:81 [binder, in RegLang.regexp]
q:81 [binder, in RegLang.nfa]
q:82 [binder, in RegLang.misc]
q:82 [binder, in RegLang.shepherdson]
q:85 [binder, in RegLang.wmso]
q:85 [binder, in RegLang.shepherdson]
q:86 [binder, in RegLang.nfa]
q:87 [binder, in RegLang.shepherdson]
q:88 [binder, in RegLang.shepherdson]
q:91 [binder, in RegLang.wmso]
q:94 [binder, in RegLang.wmso]
q:99 [binder, in RegLang.shepherdson]
R
R [definition, in RegLang.regexp]R [definition, in RegLang.two_way]
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_predType [definition, in RegLang.regexp]
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_correct [lemma, in RegLang.regexp]
rev_flatten [lemma, in RegLang.misc]
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]
rT:152 [binder, in RegLang.misc]
rT:156 [binder, in RegLang.misc]
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_trans [lemma, in RegLang.nfa]
run_last [lemma, in RegLang.nfa]
run_size [lemma, in RegLang.nfa]
run_table [definition, in RegLang.vardi]
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]
r:127 [binder, in RegLang.nfa]
r:130 [binder, in RegLang.nfa]
r:132 [binder, in RegLang.nfa]
r:136 [binder, in RegLang.nfa]
r:139 [binder, in RegLang.nfa]
r:142 [binder, in RegLang.nfa]
r:144 [binder, in RegLang.shepherdson]
r:147 [binder, in RegLang.nfa]
r:15 [binder, in RegLang.regexp]
r:157 [binder, in RegLang.regexp]
r:160 [binder, in RegLang.regexp]
r:164 [binder, in RegLang.regexp]
r:166 [binder, in RegLang.regexp]
r:35 [binder, in RegLang.regexp]
r:40 [binder, in RegLang.languages]
r:41 [binder, in RegLang.regexp]
r:44 [binder, in RegLang.regexp]
r:46 [binder, in RegLang.regexp]
r:48 [binder, in RegLang.regexp]
r:50 [binder, 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]
Sf:165 [binder, in RegLang.misc]
Sf:170 [binder, in RegLang.misc]
shepherdson [library]
single [definition, in RegLang.wmso]
size_induction [lemma, in RegLang.misc]
size_glue [lemma, in RegLang.wmso]
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]
ss:38 [binder, in RegLang.misc]
ss:41 [binder, in RegLang.misc]
Star [constructor, in RegLang.regexp]
star [definition, in RegLang.languages]
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]
sT:106 [binder, in RegLang.misc]
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]
s:12 [binder, in RegLang.wmso]
s:135 [binder, in RegLang.nfa]
s:137 [binder, in RegLang.wmso]
s:146 [binder, in RegLang.nfa]
s:148 [binder, in RegLang.wmso]
s:15 [binder, in RegLang.nfa]
s:156 [binder, in RegLang.wmso]
s:158 [binder, in RegLang.regexp]
s:161 [binder, in RegLang.regexp]
s:162 [binder, in RegLang.wmso]
s:18 [binder, in RegLang.wmso]
s:196 [binder, in RegLang.dfa]
s:198 [binder, in RegLang.dfa]
s:199 [binder, in RegLang.wmso]
s:211 [binder, in RegLang.wmso]
s:213 [binder, in RegLang.wmso]
s:214 [binder, in RegLang.wmso]
s:217 [binder, in RegLang.wmso]
s:219 [binder, in RegLang.wmso]
s:221 [binder, in RegLang.wmso]
s:222 [binder, in RegLang.wmso]
s:224 [binder, in RegLang.wmso]
s:226 [binder, in RegLang.wmso]
s:229 [binder, in RegLang.wmso]
s:23 [binder, in RegLang.misc]
s:231 [binder, in RegLang.wmso]
s:234 [binder, in RegLang.wmso]
s:236 [binder, in RegLang.wmso]
s:239 [binder, in RegLang.wmso]
s:241 [binder, in RegLang.wmso]
s:243 [binder, in RegLang.wmso]
s:245 [binder, in RegLang.wmso]
s:26 [binder, in RegLang.misc]
s:262 [binder, in RegLang.wmso]
s:268 [binder, in RegLang.wmso]
s:275 [binder, in RegLang.wmso]
s:280 [binder, in RegLang.wmso]
s:282 [binder, in RegLang.wmso]
s:284 [binder, in RegLang.wmso]
s:286 [binder, in RegLang.wmso]
s:30 [binder, in RegLang.misc]
s:31 [binder, in RegLang.wmso]
s:323 [binder, in RegLang.wmso]
s:325 [binder, in RegLang.wmso]
s:33 [binder, in RegLang.nfa]
s:34 [binder, in RegLang.nfa]
s:35 [binder, in RegLang.wmso]
s:36 [binder, in RegLang.misc]
s:39 [binder, in RegLang.misc]
s:41 [binder, in RegLang.languages]
s:44 [binder, in RegLang.misc]
s:49 [binder, in RegLang.regexp]
s:49 [binder, in RegLang.two_way]
s:50 [binder, in RegLang.misc]
s:51 [binder, in RegLang.regexp]
s:52 [binder, in RegLang.wmso]
s:54 [binder, in RegLang.wmso]
s:55 [binder, in RegLang.dfa]
s:56 [binder, in RegLang.wmso]
s:60 [binder, in RegLang.misc]
s:65 [binder, in RegLang.misc]
s:72 [binder, in RegLang.misc]
s:94 [binder, in RegLang.dfa]
s:96 [binder, in RegLang.wmso]
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_uniq [lemma, in RegLang.misc]
term_srel [lemma, in RegLang.shepherdson]
tnthL [lemma, in RegLang.shepherdson]
tnthR [lemma, in RegLang.shepherdson]
trans_b0 [definition, in RegLang.wmso]
TT [definition, in RegLang.wmso]
two_way [library]
T':160 [binder, in RegLang.misc]
T':91 [binder, in RegLang.misc]
T1 [lemma, in RegLang.setoid_leq]
T1:10 [binder, in RegLang.misc]
T1:12 [binder, in RegLang.misc]
T1:6 [binder, in RegLang.misc]
T2 [lemma, in RegLang.setoid_leq]
T2:11 [binder, in RegLang.misc]
T2:13 [binder, in RegLang.misc]
T2:7 [binder, in RegLang.misc]
T:1 [binder, in RegLang.wmso]
T:10 [binder, in RegLang.shepherdson]
T:103 [binder, in RegLang.misc]
T:104 [binder, in RegLang.misc]
T:111 [binder, in RegLang.misc]
T:114 [binder, in RegLang.misc]
T:13 [binder, in RegLang.regexp]
T:148 [binder, in RegLang.misc]
T:159 [binder, in RegLang.misc]
T:16 [binder, in RegLang.vardi]
T:193 [binder, in RegLang.dfa]
T:197 [binder, in RegLang.dfa]
T:20 [binder, in RegLang.misc]
T:21 [binder, in RegLang.regexp]
t:227 [binder, in RegLang.wmso]
t:232 [binder, in RegLang.wmso]
t:235 [binder, in RegLang.wmso]
t:237 [binder, in RegLang.wmso]
t:240 [binder, in RegLang.wmso]
t:242 [binder, in RegLang.wmso]
T:25 [binder, in RegLang.misc]
T:261 [binder, in RegLang.wmso]
T:267 [binder, in RegLang.wmso]
T:274 [binder, in RegLang.wmso]
T:29 [binder, in RegLang.misc]
t:3 [binder, in RegLang.wmso]
T:33 [binder, in RegLang.regexp]
T:33 [binder, in RegLang.misc]
T:33 [binder, in RegLang.vardi]
T:37 [binder, in RegLang.misc]
T:4 [binder, in RegLang.vardi]
T:40 [binder, in RegLang.misc]
T:42 [binder, in RegLang.misc]
T:43 [binder, in RegLang.two_way]
T:48 [binder, in RegLang.misc]
T:5 [binder, in RegLang.shepherdson]
T:53 [binder, in RegLang.dfa]
T:58 [binder, in RegLang.misc]
T:64 [binder, in RegLang.misc]
T:74 [binder, in RegLang.misc]
T:77 [binder, in RegLang.misc]
T:80 [binder, in RegLang.misc]
T:85 [binder, in RegLang.misc]
T:90 [binder, in RegLang.misc]
T:96 [binder, in RegLang.misc]
U
u:13 [binder, in RegLang.myhill_nerode]u:165 [binder, in RegLang.wmso]
u:170 [binder, in RegLang.wmso]
u:171 [binder, in RegLang.wmso]
u:172 [binder, in RegLang.wmso]
u:209 [binder, in RegLang.dfa]
u:219 [binder, in RegLang.dfa]
u:38 [binder, in RegLang.myhill_nerode]
u:7 [binder, in RegLang.myhill_nerode]
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 [constructor, in RegLang.regexp]
void [definition, in RegLang.languages]
vs:139 [binder, in RegLang.wmso]
vv:19 [binder, in RegLang.languages]
vv:58 [binder, in RegLang.languages]
vv:59 [binder, in RegLang.languages]
vv:64 [binder, in RegLang.languages]
v1:180 [binder, in RegLang.wmso]
v1:184 [binder, in RegLang.wmso]
v2:181 [binder, in RegLang.wmso]
v2:185 [binder, in RegLang.wmso]
v:105 [binder, in RegLang.wmso]
v:11 [binder, in RegLang.languages]
v:118 [binder, in RegLang.wmso]
v:121 [binder, in RegLang.wmso]
v:126 [binder, in RegLang.wmso]
v:129 [binder, in RegLang.wmso]
v:13 [binder, in RegLang.languages]
v:135 [binder, in RegLang.wmso]
v:14 [binder, in RegLang.myhill_nerode]
v:150 [binder, in RegLang.wmso]
v:154 [binder, in RegLang.wmso]
v:164 [binder, in RegLang.wmso]
v:169 [binder, in RegLang.wmso]
v:175 [binder, in RegLang.wmso]
v:179 [binder, in RegLang.wmso]
v:181 [binder, in RegLang.regexp]
v:187 [binder, in RegLang.wmso]
v:193 [binder, in RegLang.wmso]
v:198 [binder, in RegLang.wmso]
v:210 [binder, in RegLang.dfa]
v:220 [binder, in RegLang.dfa]
v:34 [binder, in RegLang.languages]
v:37 [binder, in RegLang.languages]
v:39 [binder, in RegLang.wmso]
v:39 [binder, in RegLang.myhill_nerode]
v:53 [binder, in RegLang.wmso]
v:57 [binder, in RegLang.languages]
v:6 [binder, in RegLang.languages]
v:65 [binder, in RegLang.languages]
v:65 [binder, in RegLang.wmso]
v:8 [binder, in RegLang.myhill_nerode]
v:81 [binder, in RegLang.wmso]
v:90 [binder, in RegLang.wmso]
W
weak_coincidence [lemma, in RegLang.wmso]wmso [library]
word [abbreviation, in RegLang.dfa]
word [abbreviation, in RegLang.nfa]
word [definition, in RegLang.languages]
word [abbreviation, in RegLang.minimization]
word [abbreviation, in RegLang.myhill_nerode]
word_eqType [definition, in RegLang.languages]
w1:105 [binder, in RegLang.regexp]
w1:14 [binder, in RegLang.languages]
w1:46 [binder, in RegLang.languages]
w1:48 [binder, in RegLang.languages]
w1:60 [binder, in RegLang.languages]
w1:84 [binder, in RegLang.regexp]
w1:93 [binder, in RegLang.regexp]
w1:99 [binder, in RegLang.regexp]
w2:100 [binder, in RegLang.regexp]
w2:106 [binder, in RegLang.regexp]
w2:15 [binder, in RegLang.languages]
w2:47 [binder, in RegLang.languages]
w2:49 [binder, in RegLang.languages]
w2:61 [binder, in RegLang.languages]
w2:85 [binder, in RegLang.regexp]
w2:94 [binder, in RegLang.regexp]
w:10 [binder, in RegLang.languages]
w:101 [binder, in RegLang.wmso]
w:109 [binder, in RegLang.regexp]
w:109 [binder, in RegLang.wmso]
w:112 [binder, in RegLang.wmso]
w:119 [binder, in RegLang.regexp]
w:124 [binder, in RegLang.regexp]
w:133 [binder, in RegLang.shepherdson]
w:14 [binder, in RegLang.nfa]
w:151 [binder, in RegLang.nfa]
w:158 [binder, in RegLang.wmso]
w:16 [binder, in RegLang.regexp]
w:162 [binder, in RegLang.regexp]
w:167 [binder, in RegLang.regexp]
w:168 [binder, in RegLang.dfa]
w:169 [binder, in RegLang.regexp]
w:17 [binder, in RegLang.languages]
w:172 [binder, in RegLang.regexp]
w:184 [binder, in RegLang.dfa]
w:193 [binder, in RegLang.regexp]
w:20 [binder, in RegLang.dfa]
w:211 [binder, in RegLang.dfa]
w:22 [binder, in RegLang.shepherdson]
w:221 [binder, in RegLang.dfa]
w:24 [binder, in RegLang.regexp]
w:25 [binder, in RegLang.dfa]
w:25 [binder, in RegLang.languages]
w:25 [binder, in RegLang.minimization]
w:27 [binder, in RegLang.minimization]
w:28 [binder, in RegLang.languages]
w:31 [binder, in RegLang.languages]
w:334 [binder, in RegLang.wmso]
w:35 [binder, in RegLang.dfa]
w:368 [binder, in RegLang.wmso]
w:39 [binder, in RegLang.dfa]
w:40 [binder, in RegLang.myhill_nerode]
w:42 [binder, in RegLang.languages]
w:42 [binder, in RegLang.wmso]
w:43 [binder, in RegLang.dfa]
w:45 [binder, in RegLang.languages]
w:47 [binder, in RegLang.wmso]
w:5 [binder, in RegLang.minimization]
w:50 [binder, in RegLang.wmso]
w:55 [binder, in RegLang.wmso]
w:58 [binder, in RegLang.two_way]
w:61 [binder, in RegLang.regexp]
w:63 [binder, in RegLang.minimization]
w:7 [binder, in RegLang.languages]
w:76 [binder, in RegLang.regexp]
w:80 [binder, in RegLang.wmso]
w:83 [binder, in RegLang.regexp]
w:9 [binder, in RegLang.nfa]
X
xi:119 [binder, in RegLang.shepherdson]xj:120 [binder, in RegLang.shepherdson]
xk:118 [binder, in RegLang.shepherdson]
x0:21 [binder, in RegLang.misc]
x1:107 [binder, in RegLang.nfa]
x1:116 [binder, in RegLang.nfa]
x1:93 [binder, in RegLang.nfa]
x1:98 [binder, in RegLang.nfa]
x2:108 [binder, in RegLang.nfa]
x2:117 [binder, in RegLang.nfa]
x2:94 [binder, in RegLang.nfa]
x2:99 [binder, in RegLang.nfa]
x:1 [binder, in RegLang.misc]
X:10 [binder, in RegLang.myhill_nerode]
x:100 [binder, in RegLang.nfa]
X:101 [binder, in RegLang.regexp]
x:101 [binder, in RegLang.shepherdson]
x:102 [binder, in RegLang.regexp]
X:107 [binder, in RegLang.regexp]
x:107 [binder, in RegLang.misc]
x:11 [binder, in RegLang.setoid_leq]
x:11 [binder, in RegLang.shepherdson]
X:110 [binder, in RegLang.regexp]
x:110 [binder, in RegLang.nfa]
x:110 [binder, in RegLang.shepherdson]
x:111 [binder, in RegLang.regexp]
x:112 [binder, in RegLang.nfa]
x:113 [binder, in RegLang.misc]
x:114 [binder, in RegLang.dfa]
x:114 [binder, in RegLang.regexp]
x:114 [binder, in RegLang.nfa]
x:115 [binder, in RegLang.misc]
x:117 [binder, in RegLang.regexp]
x:118 [binder, in RegLang.nfa]
x:12 [binder, in RegLang.vardi]
x:122 [binder, in RegLang.regexp]
x:124 [binder, in RegLang.dfa]
x:124 [binder, in RegLang.shepherdson]
x:125 [binder, in RegLang.regexp]
x:126 [binder, in RegLang.nfa]
x:128 [binder, in RegLang.nfa]
X:129 [binder, in RegLang.regexp]
x:130 [binder, in RegLang.regexp]
x:130 [binder, in RegLang.misc]
x:131 [binder, in RegLang.nfa]
x:132 [binder, in RegLang.misc]
x:134 [binder, in RegLang.dfa]
X:134 [binder, in RegLang.regexp]
x:134 [binder, in RegLang.nfa]
x:135 [binder, in RegLang.regexp]
x:135 [binder, in RegLang.misc]
x:135 [binder, in RegLang.shepherdson]
x:137 [binder, in RegLang.nfa]
x:138 [binder, in RegLang.shepherdson]
x:139 [binder, in RegLang.misc]
x:14 [binder, in RegLang.dfa]
X:14 [binder, in RegLang.misc]
x:140 [binder, in RegLang.nfa]
x:141 [binder, in RegLang.regexp]
x:141 [binder, in RegLang.shepherdson]
x:142 [binder, in RegLang.regexp]
x:142 [binder, in RegLang.misc]
x:145 [binder, in RegLang.dfa]
x:145 [binder, in RegLang.nfa]
x:145 [binder, in RegLang.shepherdson]
x:146 [binder, in RegLang.dfa]
x:146 [binder, in RegLang.misc]
x:146 [binder, in RegLang.shepherdson]
x:148 [binder, in RegLang.regexp]
x:15 [binder, in RegLang.minimization]
x:15 [binder, in RegLang.wmso]
x:15 [binder, in RegLang.vardi]
x:154 [binder, in RegLang.dfa]
x:154 [binder, in RegLang.nfa]
x:155 [binder, in RegLang.regexp]
x:155 [binder, in RegLang.misc]
x:159 [binder, in RegLang.dfa]
x:16 [binder, in RegLang.dfa]
X:162 [binder, in RegLang.misc]
X:166 [binder, in RegLang.wmso]
X:167 [binder, in RegLang.misc]
x:17 [binder, in RegLang.misc]
x:17 [binder, in RegLang.minimization]
x:171 [binder, in RegLang.misc]
x:174 [binder, in RegLang.dfa]
X:174 [binder, in RegLang.wmso]
X:176 [binder, in RegLang.wmso]
x:18 [binder, in RegLang.misc]
x:18 [binder, in RegLang.shepherdson]
X:188 [binder, in RegLang.wmso]
x:19 [binder, in RegLang.dfa]
x:19 [binder, in RegLang.regexp]
X:190 [binder, in RegLang.wmso]
x:196 [binder, in RegLang.regexp]
x:20 [binder, in RegLang.regexp]
X:202 [binder, in RegLang.wmso]
x:203 [binder, in RegLang.dfa]
x:206 [binder, in RegLang.dfa]
X:207 [binder, in RegLang.wmso]
x:21 [binder, in RegLang.dfa]
x:21 [binder, in RegLang.languages]
x:216 [binder, in RegLang.dfa]
x:22 [binder, in RegLang.misc]
x:23 [binder, in RegLang.dfa]
x:23 [binder, in RegLang.shepherdson]
X:24 [binder, in RegLang.wmso]
x:24 [binder, in RegLang.shepherdson]
X:247 [binder, in RegLang.wmso]
X:249 [binder, in RegLang.wmso]
X:251 [binder, in RegLang.wmso]
X:253 [binder, in RegLang.wmso]
X:255 [binder, in RegLang.wmso]
x:26 [binder, in RegLang.dfa]
x:26 [binder, in RegLang.minimization]
x:263 [binder, in RegLang.wmso]
X:27 [binder, in RegLang.vardi]
x:271 [binder, in RegLang.wmso]
x:272 [binder, in RegLang.wmso]
x:279 [binder, in RegLang.wmso]
x:28 [binder, in RegLang.nfa]
x:28 [binder, in RegLang.minimization]
x:28 [binder, in RegLang.shepherdson]
x:288 [binder, in RegLang.wmso]
x:29 [binder, in RegLang.dfa]
x:29 [binder, in RegLang.languages]
X:291 [binder, in RegLang.wmso]
X:294 [binder, in RegLang.wmso]
x:295 [binder, in RegLang.wmso]
X:298 [binder, in RegLang.wmso]
x:3 [binder, in RegLang.minimization]
x:3 [binder, in RegLang.vardi]
X:30 [binder, in RegLang.vardi]
x:30 [binder, in RegLang.myhill_nerode]
X:300 [binder, in RegLang.wmso]
X:301 [binder, in RegLang.wmso]
X:304 [binder, in RegLang.wmso]
x:305 [binder, in RegLang.wmso]
x:31 [binder, in RegLang.nfa]
X:31 [binder, in RegLang.vardi]
x:310 [binder, in RegLang.wmso]
X:314 [binder, in RegLang.wmso]
X:318 [binder, in RegLang.wmso]
x:32 [binder, in RegLang.dfa]
x:32 [binder, in RegLang.nfa]
x:32 [binder, in RegLang.vardi]
x:32 [binder, in RegLang.myhill_nerode]
X:336 [binder, in RegLang.wmso]
x:338 [binder, in RegLang.wmso]
x:34 [binder, in RegLang.dfa]
x:34 [binder, in RegLang.minimization]
x:34 [binder, in RegLang.shepherdson]
X:340 [binder, in RegLang.wmso]
X:345 [binder, in RegLang.wmso]
x:346 [binder, in RegLang.wmso]
x:35 [binder, in RegLang.minimization]
X:35 [binder, in RegLang.myhill_nerode]
x:36 [binder, in RegLang.minimization]
X:36 [binder, in RegLang.wmso]
X:361 [binder, in RegLang.wmso]
x:38 [binder, in RegLang.minimization]
x:39 [binder, in RegLang.nfa]
x:39 [binder, in RegLang.shepherdson]
x:40 [binder, in RegLang.dfa]
x:40 [binder, in RegLang.minimization]
X:40 [binder, in RegLang.wmso]
x:43 [binder, in RegLang.shepherdson]
x:44 [binder, in RegLang.minimization]
X:44 [binder, in RegLang.wmso]
x:45 [binder, in RegLang.nfa]
x:45 [binder, in RegLang.two_way]
x:46 [binder, in RegLang.dfa]
x:46 [binder, in RegLang.two_way]
x:47 [binder, in RegLang.minimization]
x:49 [binder, in RegLang.dfa]
x:49 [binder, in RegLang.nfa]
X:5 [binder, in RegLang.myhill_nerode]
x:50 [binder, in RegLang.two_way]
X:51 [binder, in RegLang.nfa]
x:51 [binder, in RegLang.shepherdson]
x:52 [binder, in RegLang.dfa]
x:52 [binder, in RegLang.misc]
x:53 [binder, in RegLang.misc]
X:54 [binder, in RegLang.regexp]
x:54 [binder, in RegLang.misc]
X:55 [binder, in RegLang.nfa]
x:55 [binder, in RegLang.misc]
x:55 [binder, in RegLang.minimization]
x:56 [binder, in RegLang.dfa]
x:57 [binder, in RegLang.regexp]
x:57 [binder, in RegLang.nfa]
x:57 [binder, in RegLang.minimization]
x:59 [binder, in RegLang.regexp]
x:59 [binder, in RegLang.minimization]
x:6 [binder, in RegLang.shepherdson]
x:60 [binder, in RegLang.dfa]
x:61 [binder, in RegLang.dfa]
x:61 [binder, in RegLang.minimization]
X:62 [binder, in RegLang.regexp]
x:62 [binder, in RegLang.minimization]
X:62 [binder, in RegLang.wmso]
x:62 [binder, in RegLang.shepherdson]
x:64 [binder, in RegLang.minimization]
x:65 [binder, in RegLang.regexp]
x:67 [binder, in RegLang.dfa]
X:67 [binder, in RegLang.regexp]
x:68 [binder, in RegLang.regexp]
X:68 [binder, in RegLang.wmso]
x:69 [binder, in RegLang.shepherdson]
x:71 [binder, in RegLang.dfa]
X:71 [binder, in RegLang.regexp]
x:72 [binder, in RegLang.regexp]
x:74 [binder, in RegLang.dfa]
x:75 [binder, in RegLang.misc]
X:77 [binder, in RegLang.wmso]
x:78 [binder, in RegLang.misc]
x:79 [binder, in RegLang.dfa]
X:79 [binder, in RegLang.regexp]
x:8 [binder, in RegLang.nfa]
x:8 [binder, in RegLang.minimization]
x:81 [binder, in RegLang.dfa]
x:83 [binder, in RegLang.misc]
x:84 [binder, in RegLang.dfa]
x:84 [binder, in RegLang.misc]
x:86 [binder, in RegLang.dfa]
x:88 [binder, in RegLang.dfa]
x:88 [binder, in RegLang.misc]
x:89 [binder, in RegLang.dfa]
X:89 [binder, in RegLang.regexp]
x:89 [binder, in RegLang.misc]
x:9 [binder, in RegLang.dfa]
x:9 [binder, in RegLang.setoid_leq]
x:9 [binder, in RegLang.vardi]
x:90 [binder, in RegLang.regexp]
x:91 [binder, in RegLang.dfa]
x:91 [binder, in RegLang.nfa]
X:93 [binder, in RegLang.misc]
x:95 [binder, in RegLang.dfa]
X:95 [binder, in RegLang.regexp]
x:96 [binder, in RegLang.dfa]
x:96 [binder, in RegLang.regexp]
x:96 [binder, in RegLang.nfa]
x:97 [binder, in RegLang.dfa]
x:98 [binder, in RegLang.dfa]
x:98 [binder, in RegLang.misc]
Y
yi:122 [binder, in RegLang.shepherdson]yj:123 [binder, in RegLang.shepherdson]
yk:121 [binder, in RegLang.shepherdson]
y:10 [binder, in RegLang.setoid_leq]
y:102 [binder, in RegLang.shepherdson]
y:103 [binder, in RegLang.regexp]
y:108 [binder, in RegLang.misc]
y:111 [binder, in RegLang.shepherdson]
y:112 [binder, in RegLang.regexp]
y:115 [binder, in RegLang.regexp]
y:118 [binder, in RegLang.regexp]
y:12 [binder, in RegLang.nfa]
y:12 [binder, in RegLang.setoid_leq]
y:123 [binder, in RegLang.regexp]
y:125 [binder, in RegLang.dfa]
y:126 [binder, in RegLang.dfa]
y:126 [binder, in RegLang.regexp]
y:130 [binder, in RegLang.dfa]
y:131 [binder, in RegLang.dfa]
y:131 [binder, in RegLang.regexp]
y:131 [binder, in RegLang.misc]
y:133 [binder, in RegLang.misc]
y:136 [binder, in RegLang.regexp]
y:136 [binder, in RegLang.misc]
y:139 [binder, in RegLang.dfa]
y:140 [binder, in RegLang.dfa]
y:140 [binder, in RegLang.misc]
y:143 [binder, in RegLang.regexp]
y:144 [binder, in RegLang.dfa]
y:144 [binder, in RegLang.misc]
y:147 [binder, in RegLang.misc]
y:150 [binder, in RegLang.dfa]
y:151 [binder, in RegLang.dfa]
y:154 [binder, in RegLang.misc]
y:155 [binder, in RegLang.dfa]
y:16 [binder, in RegLang.wmso]
Y:163 [binder, in RegLang.misc]
y:166 [binder, in RegLang.misc]
Y:167 [binder, in RegLang.wmso]
Y:168 [binder, in RegLang.misc]
y:17 [binder, in RegLang.dfa]
y:175 [binder, in RegLang.dfa]
Y:177 [binder, in RegLang.wmso]
y:19 [binder, in RegLang.misc]
Y:191 [binder, in RegLang.wmso]
y:207 [binder, in RegLang.dfa]
y:217 [binder, in RegLang.dfa]
y:289 [binder, in RegLang.wmso]
Y:29 [binder, in RegLang.vardi]
Y:292 [binder, in RegLang.wmso]
Y:296 [binder, in RegLang.wmso]
y:297 [binder, in RegLang.wmso]
Y:302 [binder, in RegLang.wmso]
Y:306 [binder, in RegLang.wmso]
y:307 [binder, in RegLang.wmso]
y:4 [binder, in RegLang.minimization]
y:48 [binder, in RegLang.minimization]
y:58 [binder, in RegLang.minimization]
y:59 [binder, in RegLang.nfa]
y:60 [binder, in RegLang.regexp]
Y:63 [binder, in RegLang.wmso]
y:68 [binder, in RegLang.dfa]
y:69 [binder, in RegLang.regexp]
Y:69 [binder, in RegLang.wmso]
y:72 [binder, in RegLang.dfa]
y:73 [binder, in RegLang.regexp]
y:76 [binder, in RegLang.misc]
Y:78 [binder, in RegLang.wmso]
y:9 [binder, in RegLang.minimization]
y:91 [binder, in RegLang.regexp]
y:92 [binder, in RegLang.dfa]
Y:94 [binder, in RegLang.misc]
y:97 [binder, in RegLang.regexp]
Z
zero [definition, in RegLang.wmso]zero_at [definition, in RegLang.wmso]
z:103 [binder, in RegLang.shepherdson]
z:104 [binder, in RegLang.regexp]
z:108 [binder, in RegLang.regexp]
z:112 [binder, in RegLang.shepherdson]
z:113 [binder, in RegLang.regexp]
z:12 [binder, in RegLang.shepherdson]
z:134 [binder, in RegLang.misc]
z:137 [binder, in RegLang.regexp]
z:137 [binder, in RegLang.misc]
z:138 [binder, in RegLang.regexp]
z:139 [binder, in RegLang.regexp]
z:140 [binder, in RegLang.regexp]
z:143 [binder, in RegLang.misc]
z:208 [binder, in RegLang.dfa]
z:218 [binder, in RegLang.dfa]
z:7 [binder, in RegLang.shepherdson]
z:70 [binder, in RegLang.regexp]
z:70 [binder, in RegLang.shepherdson]
z:73 [binder, in RegLang.dfa]
z:82 [binder, in RegLang.regexp]
z:92 [binder, in RegLang.regexp]
z:98 [binder, in RegLang.regexp]
other
_ <-T-> _ [notation, in RegLang.misc]_ =p _ [notation, in RegLang.misc]
_ <--> _ [notation, in RegLang.wmso]
_ :\/: _ [notation, in RegLang.wmso]
_ :/\: _ [notation, in RegLang.wmso]
_ --> _ [notation, in RegLang.wmso]
_ |= _ [notation, in RegLang.wmso]
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
_ <-T-> _ [in RegLang.misc]_ =p _ [in RegLang.misc]
_ <--> _ [in RegLang.wmso]
_ :\/: _ [in RegLang.wmso]
_ :/\: _ [in RegLang.wmso]
_ --> _ [in RegLang.wmso]
_ |= _ [in RegLang.wmso]
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]
Binder Index
A
aT:151 [in RegLang.misc]aT:157 [in RegLang.misc]
A1:101 [in RegLang.dfa]
A1:103 [in RegLang.dfa]
A1:107 [in RegLang.dfa]
A1:12 [in RegLang.minimization]
A1:99 [in RegLang.dfa]
A2:100 [in RegLang.dfa]
A2:102 [in RegLang.dfa]
A2:104 [in RegLang.dfa]
A2:108 [in RegLang.dfa]
A2:13 [in RegLang.minimization]
a:1 [in RegLang.setoid_leq]
A:10 [in RegLang.minimization]
a:105 [in RegLang.dfa]
A:107 [in RegLang.wmso]
A:111 [in RegLang.wmso]
A:113 [in RegLang.dfa]
a:115 [in RegLang.dfa]
A:116 [in RegLang.dfa]
a:116 [in RegLang.regexp]
a:120 [in RegLang.regexp]
a:121 [in RegLang.regexp]
a:123 [in RegLang.nfa]
a:127 [in RegLang.regexp]
a:128 [in RegLang.regexp]
A:128 [in RegLang.shepherdson]
A:129 [in RegLang.shepherdson]
a:13 [in RegLang.dfa]
A:13 [in RegLang.nfa]
A:151 [in RegLang.shepherdson]
A:152 [in RegLang.shepherdson]
a:16 [in RegLang.minimization]
a:160 [in RegLang.dfa]
a:161 [in RegLang.dfa]
A:163 [in RegLang.wmso]
a:170 [in RegLang.regexp]
a:18 [in RegLang.languages]
A:2 [in RegLang.minimization]
A:201 [in RegLang.dfa]
A:205 [in RegLang.dfa]
a:225 [in RegLang.dfa]
a:226 [in RegLang.dfa]
a:24 [in RegLang.dfa]
a:26 [in RegLang.nfa]
A:28 [in RegLang.dfa]
a:28 [in RegLang.vardi]
A:29 [in RegLang.minimization]
a:31 [in RegLang.myhill_nerode]
a:33 [in RegLang.dfa]
a:33 [in RegLang.two_way]
a:333 [in RegLang.wmso]
a:34 [in RegLang.misc]
a:354 [in RegLang.wmso]
a:37 [in RegLang.minimization]
a:39 [in RegLang.minimization]
a:4 [in RegLang.wmso]
a:41 [in RegLang.dfa]
a:41 [in RegLang.nfa]
a:43 [in RegLang.misc]
a:43 [in RegLang.wmso]
A:44 [in RegLang.two_way]
a:45 [in RegLang.dfa]
a:46 [in RegLang.wmso]
a:49 [in RegLang.misc]
a:49 [in RegLang.minimization]
a:49 [in RegLang.wmso]
a:5 [in RegLang.setoid_leq]
a:52 [in RegLang.nfa]
a:56 [in RegLang.two_way]
a:56 [in RegLang.minimization]
a:57 [in RegLang.dfa]
a:58 [in RegLang.dfa]
a:58 [in RegLang.nfa]
a:59 [in RegLang.dfa]
a:59 [in RegLang.misc]
A:59 [in RegLang.wmso]
A:6 [in RegLang.minimization]
a:60 [in RegLang.nfa]
a:60 [in RegLang.minimization]
a:62 [in RegLang.dfa]
a:63 [in RegLang.dfa]
a:64 [in RegLang.nfa]
A:65 [in RegLang.minimization]
A:66 [in RegLang.minimization]
A:67 [in RegLang.minimization]
a:68 [in RegLang.nfa]
A:68 [in RegLang.minimization]
a:69 [in RegLang.dfa]
A:69 [in RegLang.minimization]
A:7 [in RegLang.nfa]
A:7 [in RegLang.minimization]
A:70 [in RegLang.minimization]
A:71 [in RegLang.minimization]
A:72 [in RegLang.minimization]
A:73 [in RegLang.minimization]
A:74 [in RegLang.minimization]
A:75 [in RegLang.minimization]
A:76 [in RegLang.minimization]
a:77 [in RegLang.regexp]
A:77 [in RegLang.minimization]
a:78 [in RegLang.regexp]
a:80 [in RegLang.nfa]
A:83 [in RegLang.wmso]
a:87 [in RegLang.dfa]
A:88 [in RegLang.wmso]
a:9 [in RegLang.myhill_nerode]
a:93 [in RegLang.dfa]
B
bs:140 [in RegLang.wmso]bs:152 [in RegLang.wmso]
bs:99 [in RegLang.wmso]
b1:4 [in RegLang.misc]
b1:56 [in RegLang.misc]
b2:5 [in RegLang.misc]
b2:57 [in RegLang.misc]
b:1 [in RegLang.shepherdson]
b:106 [in RegLang.dfa]
b:108 [in RegLang.wmso]
B:11 [in RegLang.minimization]
b:113 [in RegLang.wmso]
b:115 [in RegLang.wmso]
b:116 [in RegLang.wmso]
b:119 [in RegLang.wmso]
b:124 [in RegLang.wmso]
b:127 [in RegLang.wmso]
b:133 [in RegLang.wmso]
b:147 [in RegLang.shepherdson]
b:2 [in RegLang.setoid_leq]
b:227 [in RegLang.dfa]
B:31 [in RegLang.minimization]
b:46 [in RegLang.misc]
b:47 [in RegLang.misc]
b:6 [in RegLang.setoid_leq]
B:60 [in RegLang.wmso]
b:62 [in RegLang.nfa]
b:62 [in RegLang.misc]
b:63 [in RegLang.misc]
B:78 [in RegLang.minimization]
b:86 [in RegLang.wmso]
b:92 [in RegLang.wmso]
C
char':118 [in RegLang.dfa]char':184 [in RegLang.regexp]
char:10 [in RegLang.regexp]
char:117 [in RegLang.dfa]
char:135 [in RegLang.dfa]
char:14 [in RegLang.regexp]
char:152 [in RegLang.regexp]
char:156 [in RegLang.regexp]
char:159 [in RegLang.regexp]
char:162 [in RegLang.dfa]
char:163 [in RegLang.regexp]
char:165 [in RegLang.regexp]
char:166 [in RegLang.dfa]
char:168 [in RegLang.regexp]
char:169 [in RegLang.dfa]
char:171 [in RegLang.regexp]
char:183 [in RegLang.regexp]
char:187 [in RegLang.regexp]
char:191 [in RegLang.regexp]
char:194 [in RegLang.regexp]
char:218 [in RegLang.wmso]
char:22 [in RegLang.regexp]
char:29 [in RegLang.regexp]
char:34 [in RegLang.regexp]
char:6 [in RegLang.regexp]
cl:58 [in RegLang.shepherdson]
cr:59 [in RegLang.shepherdson]
cs:56 [in RegLang.shepherdson]
c:101 [in RegLang.nfa]
C:13 [in RegLang.vardi]
c:19 [in RegLang.shepherdson]
c:26 [in RegLang.two_way]
c:35 [in RegLang.shepherdson]
c:40 [in RegLang.shepherdson]
c:70 [in RegLang.wmso]
c:83 [in RegLang.shepherdson]
c:84 [in RegLang.nfa]
c:84 [in RegLang.shepherdson]
c:98 [in RegLang.shepherdson]
D
decP:173 [in RegLang.misc]d:20 [in RegLang.shepherdson]
d:27 [in RegLang.two_way]
d:36 [in RegLang.shepherdson]
d:41 [in RegLang.shepherdson]
E
e1:149 [in RegLang.misc]e1:4 [in RegLang.regexp]
e2:150 [in RegLang.misc]
e2:5 [in RegLang.regexp]
e:112 [in RegLang.misc]
E:12 [in RegLang.myhill_nerode]
e:154 [in RegLang.regexp]
e:177 [in RegLang.regexp]
e:180 [in RegLang.regexp]
e:188 [in RegLang.regexp]
e:192 [in RegLang.regexp]
e:30 [in RegLang.regexp]
E:37 [in RegLang.myhill_nerode]
e:45 [in RegLang.regexp]
e:47 [in RegLang.regexp]
E:6 [in RegLang.myhill_nerode]
e:7 [in RegLang.regexp]
F
f:153 [in RegLang.misc]f:158 [in RegLang.misc]
f:161 [in RegLang.misc]
f:164 [in RegLang.misc]
f:169 [in RegLang.misc]
F:17 [in RegLang.regexp]
f:176 [in RegLang.dfa]
F:25 [in RegLang.regexp]
F:264 [in RegLang.wmso]
F:269 [in RegLang.wmso]
F:276 [in RegLang.wmso]
f:30 [in RegLang.minimization]
F:36 [in RegLang.regexp]
f:64 [in RegLang.two_way]
f:66 [in RegLang.two_way]
F:67 [in RegLang.misc]
f:92 [in RegLang.misc]
f:95 [in RegLang.misc]
H
Hi:144 [in RegLang.nfa]h:119 [in RegLang.dfa]
H:137 [in RegLang.shepherdson]
h:185 [in RegLang.regexp]
H:26 [in RegLang.myhill_nerode]
H:65 [in RegLang.myhill_nerode]
I
i':12 [in RegLang.two_way]I':23 [in RegLang.wmso]
I':28 [in RegLang.wmso]
I':30 [in RegLang.wmso]
I':34 [in RegLang.wmso]
i:10 [in RegLang.vardi]
i:106 [in RegLang.shepherdson]
i:11 [in RegLang.regexp]
i:11 [in RegLang.two_way]
I:11 [in RegLang.wmso]
i:115 [in RegLang.shepherdson]
i:119 [in RegLang.misc]
i:12 [in RegLang.regexp]
i:120 [in RegLang.misc]
i:123 [in RegLang.wmso]
i:13 [in RegLang.shepherdson]
i:130 [in RegLang.wmso]
i:132 [in RegLang.wmso]
i:14 [in RegLang.minimization]
i:14 [in RegLang.vardi]
i:141 [in RegLang.wmso]
i:143 [in RegLang.nfa]
i:143 [in RegLang.wmso]
i:148 [in RegLang.nfa]
i:159 [in RegLang.wmso]
i:160 [in RegLang.wmso]
i:18 [in RegLang.regexp]
i:194 [in RegLang.dfa]
i:194 [in RegLang.wmso]
i:195 [in RegLang.wmso]
i:196 [in RegLang.wmso]
I:200 [in RegLang.wmso]
i:204 [in RegLang.dfa]
I:204 [in RegLang.wmso]
i:206 [in RegLang.wmso]
I:208 [in RegLang.wmso]
I:210 [in RegLang.wmso]
i:212 [in RegLang.dfa]
I:212 [in RegLang.wmso]
i:213 [in RegLang.dfa]
I:215 [in RegLang.wmso]
I:22 [in RegLang.wmso]
I:220 [in RegLang.wmso]
i:222 [in RegLang.dfa]
I:223 [in RegLang.wmso]
I:225 [in RegLang.wmso]
I:228 [in RegLang.wmso]
I:230 [in RegLang.wmso]
I:233 [in RegLang.wmso]
I:238 [in RegLang.wmso]
I:244 [in RegLang.wmso]
I:248 [in RegLang.wmso]
I:250 [in RegLang.wmso]
I:254 [in RegLang.wmso]
i:257 [in RegLang.wmso]
i:258 [in RegLang.wmso]
i:259 [in RegLang.wmso]
i:26 [in RegLang.regexp]
i:260 [in RegLang.wmso]
I:265 [in RegLang.wmso]
i:266 [in RegLang.wmso]
i:27 [in RegLang.regexp]
I:27 [in RegLang.wmso]
I:270 [in RegLang.wmso]
i:273 [in RegLang.wmso]
I:277 [in RegLang.wmso]
i:278 [in RegLang.wmso]
i:28 [in RegLang.regexp]
I:281 [in RegLang.wmso]
I:285 [in RegLang.wmso]
I:29 [in RegLang.wmso]
I:293 [in RegLang.wmso]
I:299 [in RegLang.wmso]
i:30 [in RegLang.shepherdson]
I:303 [in RegLang.wmso]
I:309 [in RegLang.wmso]
I:311 [in RegLang.wmso]
I:315 [in RegLang.wmso]
I:319 [in RegLang.wmso]
I:326 [in RegLang.wmso]
I:33 [in RegLang.wmso]
i:34 [in RegLang.vardi]
I:341 [in RegLang.wmso]
i:35 [in RegLang.languages]
I:351 [in RegLang.wmso]
I:358 [in RegLang.wmso]
i:36 [in RegLang.vardi]
I:365 [in RegLang.wmso]
i:369 [in RegLang.wmso]
i:37 [in RegLang.vardi]
i:371 [in RegLang.wmso]
i:374 [in RegLang.wmso]
i:375 [in RegLang.wmso]
i:377 [in RegLang.wmso]
i:38 [in RegLang.regexp]
i:38 [in RegLang.vardi]
i:39 [in RegLang.regexp]
i:41 [in RegLang.wmso]
i:46 [in RegLang.shepherdson]
i:5 [in RegLang.two_way]
i:5 [in RegLang.vardi]
i:52 [in RegLang.shepherdson]
i:58 [in RegLang.regexp]
i:59 [in RegLang.two_way]
i:63 [in RegLang.two_way]
i:63 [in RegLang.shepherdson]
i:66 [in RegLang.regexp]
i:67 [in RegLang.two_way]
i:70 [in RegLang.misc]
i:73 [in RegLang.misc]
i:75 [in RegLang.dfa]
i:75 [in RegLang.shepherdson]
i:79 [in RegLang.shepherdson]
I:8 [in RegLang.wmso]
i:8 [in RegLang.shepherdson]
i:82 [in RegLang.dfa]
i:86 [in RegLang.regexp]
i:87 [in RegLang.regexp]
i:88 [in RegLang.regexp]
J
j:107 [in RegLang.shepherdson]j:116 [in RegLang.shepherdson]
j:14 [in RegLang.shepherdson]
j:195 [in RegLang.dfa]
j:32 [in RegLang.shepherdson]
j:35 [in RegLang.vardi]
j:47 [in RegLang.shepherdson]
j:48 [in RegLang.two_way]
j:53 [in RegLang.shepherdson]
j:64 [in RegLang.shepherdson]
j:7 [in RegLang.vardi]
j:76 [in RegLang.dfa]
j:76 [in RegLang.shepherdson]
j:80 [in RegLang.shepherdson]
j:9 [in RegLang.shepherdson]
K
k':100 [in RegLang.shepherdson]k':37 [in RegLang.shepherdson]
k':50 [in RegLang.shepherdson]
k':61 [in RegLang.shepherdson]
k':92 [in RegLang.shepherdson]
k:108 [in RegLang.shepherdson]
k:117 [in RegLang.shepherdson]
k:122 [in RegLang.wmso]
k:131 [in RegLang.wmso]
k:132 [in RegLang.shepherdson]
k:134 [in RegLang.shepherdson]
k:136 [in RegLang.wmso]
k:142 [in RegLang.wmso]
k:144 [in RegLang.wmso]
k:145 [in RegLang.wmso]
k:146 [in RegLang.wmso]
k:147 [in RegLang.wmso]
k:151 [in RegLang.wmso]
k:155 [in RegLang.wmso]
k:17 [in RegLang.shepherdson]
k:189 [in RegLang.wmso]
k:21 [in RegLang.shepherdson]
k:215 [in RegLang.dfa]
k:27 [in RegLang.shepherdson]
k:290 [in RegLang.wmso]
k:33 [in RegLang.shepherdson]
k:342 [in RegLang.wmso]
k:352 [in RegLang.wmso]
k:38 [in RegLang.shepherdson]
k:42 [in RegLang.shepherdson]
k:45 [in RegLang.wmso]
k:48 [in RegLang.wmso]
k:49 [in RegLang.shepherdson]
k:60 [in RegLang.shepherdson]
k:68 [in RegLang.misc]
k:72 [in RegLang.shepherdson]
k:89 [in RegLang.shepherdson]
k:9 [in RegLang.wmso]
k:91 [in RegLang.shepherdson]
k:96 [in RegLang.shepherdson]
L
L1:136 [in RegLang.dfa]L1:163 [in RegLang.dfa]
L1:20 [in RegLang.myhill_nerode]
L1:23 [in RegLang.languages]
L1:23 [in RegLang.myhill_nerode]
L1:26 [in RegLang.languages]
L1:30 [in RegLang.dfa]
L1:32 [in RegLang.languages]
L1:43 [in RegLang.languages]
L1:47 [in RegLang.dfa]
L1:50 [in RegLang.dfa]
L1:50 [in RegLang.languages]
l1:52 [in RegLang.languages]
L1:59 [in RegLang.myhill_nerode]
L1:62 [in RegLang.myhill_nerode]
l1:66 [in RegLang.languages]
L1:8 [in RegLang.languages]
L2:137 [in RegLang.dfa]
L2:164 [in RegLang.dfa]
L2:21 [in RegLang.myhill_nerode]
L2:24 [in RegLang.languages]
L2:24 [in RegLang.myhill_nerode]
L2:27 [in RegLang.languages]
L2:31 [in RegLang.dfa]
L2:33 [in RegLang.languages]
L2:44 [in RegLang.languages]
L2:48 [in RegLang.dfa]
L2:51 [in RegLang.dfa]
L2:51 [in RegLang.languages]
l2:53 [in RegLang.languages]
L2:60 [in RegLang.myhill_nerode]
L2:63 [in RegLang.myhill_nerode]
l2:67 [in RegLang.languages]
L2:9 [in RegLang.languages]
l3:54 [in RegLang.languages]
l4:55 [in RegLang.languages]
L:11 [in RegLang.myhill_nerode]
L:12 [in RegLang.languages]
L:120 [in RegLang.dfa]
L:15 [in RegLang.myhill_nerode]
L:152 [in RegLang.nfa]
L:153 [in RegLang.regexp]
L:167 [in RegLang.dfa]
L:173 [in RegLang.dfa]
L:177 [in RegLang.dfa]
L:186 [in RegLang.regexp]
L:195 [in RegLang.regexp]
L:214 [in RegLang.dfa]
L:22 [in RegLang.languages]
L:27 [in RegLang.dfa]
L:30 [in RegLang.languages]
L:33 [in RegLang.myhill_nerode]
L:36 [in RegLang.languages]
L:36 [in RegLang.myhill_nerode]
L:41 [in RegLang.myhill_nerode]
L:45 [in RegLang.myhill_nerode]
L:47 [in RegLang.myhill_nerode]
L:49 [in RegLang.myhill_nerode]
L:5 [in RegLang.languages]
L:51 [in RegLang.myhill_nerode]
L:53 [in RegLang.myhill_nerode]
L:54 [in RegLang.dfa]
L:55 [in RegLang.myhill_nerode]
L:56 [in RegLang.languages]
L:57 [in RegLang.myhill_nerode]
L:62 [in RegLang.languages]
L:63 [in RegLang.languages]
M
measure:15 [in RegLang.misc]M1:22 [in RegLang.myhill_nerode]
M1:25 [in RegLang.myhill_nerode]
m:117 [in RegLang.misc]
m:2 [in RegLang.two_way]
m:26 [in RegLang.wmso]
m:28 [in RegLang.misc]
M:30 [in RegLang.two_way]
m:32 [in RegLang.misc]
m:335 [in RegLang.wmso]
M:34 [in RegLang.myhill_nerode]
m:350 [in RegLang.wmso]
m:364 [in RegLang.wmso]
m:37 [in RegLang.regexp]
m:4 [in RegLang.shepherdson]
m:48 [in RegLang.shepherdson]
M:58 [in RegLang.myhill_nerode]
M:66 [in RegLang.nfa]
m:69 [in RegLang.misc]
m:7 [in RegLang.two_way]
m:7 [in RegLang.setoid_leq]
M:78 [in RegLang.nfa]
m:90 [in RegLang.shepherdson]
m:95 [in RegLang.shepherdson]
N
Ns:308 [in RegLang.wmso]Ns:313 [in RegLang.wmso]
Ns:317 [in RegLang.wmso]
Ns:321 [in RegLang.wmso]
Ns:327 [in RegLang.wmso]
Ns:349 [in RegLang.wmso]
Ns:357 [in RegLang.wmso]
Ns:363 [in RegLang.wmso]
n0:71 [in RegLang.misc]
n1:178 [in RegLang.dfa]
n1:186 [in RegLang.dfa]
n1:188 [in RegLang.dfa]
n1:190 [in RegLang.dfa]
n1:223 [in RegLang.dfa]
N1:61 [in RegLang.myhill_nerode]
N1:64 [in RegLang.myhill_nerode]
n2:179 [in RegLang.dfa]
n2:187 [in RegLang.dfa]
n2:189 [in RegLang.dfa]
n2:191 [in RegLang.dfa]
n2:224 [in RegLang.dfa]
n:1 [in RegLang.two_way]
n:10 [in RegLang.two_way]
n:100 [in RegLang.misc]
n:100 [in RegLang.wmso]
n:101 [in RegLang.misc]
n:102 [in RegLang.misc]
n:106 [in RegLang.wmso]
n:110 [in RegLang.wmso]
n:117 [in RegLang.wmso]
n:118 [in RegLang.misc]
n:120 [in RegLang.wmso]
n:121 [in RegLang.misc]
n:122 [in RegLang.misc]
n:123 [in RegLang.misc]
n:124 [in RegLang.misc]
n:125 [in RegLang.wmso]
n:128 [in RegLang.wmso]
n:134 [in RegLang.wmso]
n:138 [in RegLang.wmso]
n:145 [in RegLang.regexp]
n:149 [in RegLang.regexp]
N:149 [in RegLang.nfa]
n:149 [in RegLang.wmso]
n:150 [in RegLang.regexp]
N:150 [in RegLang.nfa]
N:153 [in RegLang.nfa]
n:153 [in RegLang.wmso]
n:157 [in RegLang.wmso]
n:161 [in RegLang.wmso]
n:168 [in RegLang.wmso]
N:17 [in RegLang.wmso]
n:173 [in RegLang.wmso]
n:178 [in RegLang.wmso]
n:180 [in RegLang.dfa]
n:185 [in RegLang.dfa]
n:186 [in RegLang.wmso]
n:192 [in RegLang.dfa]
n:192 [in RegLang.wmso]
n:197 [in RegLang.wmso]
n:199 [in RegLang.dfa]
n:2 [in RegLang.wmso]
n:201 [in RegLang.wmso]
n:203 [in RegLang.wmso]
n:205 [in RegLang.wmso]
n:209 [in RegLang.wmso]
n:21 [in RegLang.wmso]
n:216 [in RegLang.wmso]
n:24 [in RegLang.misc]
N:246 [in RegLang.wmso]
n:25 [in RegLang.two_way]
n:25 [in RegLang.wmso]
n:252 [in RegLang.wmso]
n:256 [in RegLang.wmso]
n:27 [in RegLang.misc]
n:283 [in RegLang.wmso]
n:287 [in RegLang.wmso]
n:3 [in RegLang.shepherdson]
n:31 [in RegLang.misc]
n:312 [in RegLang.wmso]
n:316 [in RegLang.wmso]
n:320 [in RegLang.wmso]
n:322 [in RegLang.wmso]
n:324 [in RegLang.wmso]
n:343 [in RegLang.wmso]
n:35 [in RegLang.misc]
n:370 [in RegLang.wmso]
n:38 [in RegLang.wmso]
N:46 [in RegLang.myhill_nerode]
N:48 [in RegLang.myhill_nerode]
N:50 [in RegLang.myhill_nerode]
n:51 [in RegLang.wmso]
N:52 [in RegLang.myhill_nerode]
N:54 [in RegLang.myhill_nerode]
N:56 [in RegLang.myhill_nerode]
n:57 [in RegLang.wmso]
n:58 [in RegLang.wmso]
n:6 [in RegLang.two_way]
n:61 [in RegLang.wmso]
N:65 [in RegLang.nfa]
n:67 [in RegLang.wmso]
N:7 [in RegLang.wmso]
n:76 [in RegLang.wmso]
N:77 [in RegLang.nfa]
n:78 [in RegLang.dfa]
n:79 [in RegLang.wmso]
n:8 [in RegLang.two_way]
n:8 [in RegLang.setoid_leq]
n:82 [in RegLang.wmso]
n:87 [in RegLang.wmso]
n:9 [in RegLang.two_way]
n:95 [in RegLang.wmso]
n:99 [in RegLang.misc]
O
o:113 [in RegLang.nfa]P
paq:347 [in RegLang.wmso]pq:26 [in RegLang.shepherdson]
Px:109 [in RegLang.misc]
Py:110 [in RegLang.misc]
p':43 [in RegLang.nfa]
p':57 [in RegLang.shepherdson]
p':67 [in RegLang.shepherdson]
p':68 [in RegLang.shepherdson]
p':94 [in RegLang.shepherdson]
P1:86 [in RegLang.misc]
P2:87 [in RegLang.misc]
p:102 [in RegLang.nfa]
p:104 [in RegLang.shepherdson]
P:105 [in RegLang.misc]
p:109 [in RegLang.nfa]
p:111 [in RegLang.nfa]
p:113 [in RegLang.shepherdson]
p:116 [in RegLang.misc]
p:12 [in RegLang.dfa]
p:122 [in RegLang.nfa]
p:124 [in RegLang.nfa]
p:129 [in RegLang.nfa]
p:13 [in RegLang.two_way]
p:133 [in RegLang.nfa]
p:138 [in RegLang.nfa]
p:139 [in RegLang.shepherdson]
p:141 [in RegLang.nfa]
p:142 [in RegLang.shepherdson]
p:149 [in RegLang.shepherdson]
p:15 [in RegLang.dfa]
p:16 [in RegLang.misc]
P:170 [in RegLang.dfa]
P:171 [in RegLang.dfa]
P:172 [in RegLang.misc]
p:18 [in RegLang.dfa]
P:2 [in RegLang.misc]
P:2 [in RegLang.shepherdson]
p:202 [in RegLang.dfa]
p:21 [in RegLang.vardi]
p:22 [in RegLang.dfa]
P:23 [in RegLang.regexp]
p:23 [in RegLang.vardi]
p:25 [in RegLang.nfa]
p:25 [in RegLang.vardi]
p:29 [in RegLang.nfa]
p:29 [in RegLang.shepherdson]
p:32 [in RegLang.two_way]
p:35 [in RegLang.nfa]
p:35 [in RegLang.two_way]
p:353 [in RegLang.wmso]
p:37 [in RegLang.nfa]
p:37 [in RegLang.two_way]
p:40 [in RegLang.nfa]
p:42 [in RegLang.minimization]
p:44 [in RegLang.nfa]
p:44 [in RegLang.shepherdson]
P:45 [in RegLang.misc]
p:45 [in RegLang.minimization]
p:46 [in RegLang.nfa]
p:47 [in RegLang.two_way]
p:50 [in RegLang.minimization]
P:51 [in RegLang.misc]
p:52 [in RegLang.minimization]
p:53 [in RegLang.minimization]
p:54 [in RegLang.nfa]
p:54 [in RegLang.shepherdson]
p:55 [in RegLang.regexp]
p:6 [in RegLang.vardi]
p:61 [in RegLang.nfa]
P:61 [in RegLang.misc]
p:63 [in RegLang.regexp]
p:64 [in RegLang.wmso]
p:65 [in RegLang.shepherdson]
P:66 [in RegLang.misc]
p:67 [in RegLang.nfa]
p:71 [in RegLang.wmso]
p:71 [in RegLang.shepherdson]
p:74 [in RegLang.regexp]
p:77 [in RegLang.dfa]
p:77 [in RegLang.shepherdson]
p:79 [in RegLang.nfa]
p:79 [in RegLang.misc]
p:8 [in RegLang.dfa]
p:80 [in RegLang.dfa]
p:80 [in RegLang.regexp]
p:81 [in RegLang.misc]
p:81 [in RegLang.shepherdson]
p:83 [in RegLang.dfa]
p:84 [in RegLang.wmso]
p:85 [in RegLang.dfa]
p:85 [in RegLang.nfa]
p:86 [in RegLang.shepherdson]
p:89 [in RegLang.wmso]
p:90 [in RegLang.nfa]
p:93 [in RegLang.wmso]
p:93 [in RegLang.shepherdson]
p:95 [in RegLang.nfa]
p:97 [in RegLang.nfa]
p:97 [in RegLang.misc]
p:97 [in RegLang.shepherdson]
Q
q':339 [in RegLang.wmso]q:103 [in RegLang.nfa]
q:105 [in RegLang.shepherdson]
q:11 [in RegLang.vardi]
q:114 [in RegLang.wmso]
q:114 [in RegLang.shepherdson]
q:125 [in RegLang.nfa]
q:129 [in RegLang.dfa]
q:133 [in RegLang.dfa]
q:136 [in RegLang.shepherdson]
q:140 [in RegLang.shepherdson]
q:143 [in RegLang.shepherdson]
q:148 [in RegLang.shepherdson]
q:149 [in RegLang.dfa]
q:150 [in RegLang.shepherdson]
q:153 [in RegLang.dfa]
q:156 [in RegLang.dfa]
q:157 [in RegLang.dfa]
q:158 [in RegLang.dfa]
q:22 [in RegLang.vardi]
q:24 [in RegLang.nfa]
q:24 [in RegLang.two_way]
q:24 [in RegLang.vardi]
q:25 [in RegLang.shepherdson]
q:26 [in RegLang.vardi]
q:27 [in RegLang.nfa]
q:28 [in RegLang.two_way]
Q:3 [in RegLang.misc]
q:30 [in RegLang.nfa]
q:31 [in RegLang.shepherdson]
q:33 [in RegLang.minimization]
q:337 [in RegLang.wmso]
q:344 [in RegLang.wmso]
q:355 [in RegLang.wmso]
q:356 [in RegLang.wmso]
q:359 [in RegLang.wmso]
q:36 [in RegLang.nfa]
q:360 [in RegLang.wmso]
q:362 [in RegLang.wmso]
q:366 [in RegLang.wmso]
q:367 [in RegLang.wmso]
q:376 [in RegLang.wmso]
q:38 [in RegLang.nfa]
q:42 [in RegLang.dfa]
q:42 [in RegLang.nfa]
q:43 [in RegLang.minimization]
q:44 [in RegLang.dfa]
q:45 [in RegLang.shepherdson]
q:46 [in RegLang.minimization]
q:47 [in RegLang.nfa]
q:48 [in RegLang.nfa]
q:51 [in RegLang.minimization]
q:53 [in RegLang.nfa]
q:53 [in RegLang.two_way]
q:54 [in RegLang.two_way]
q:54 [in RegLang.minimization]
q:55 [in RegLang.two_way]
q:55 [in RegLang.shepherdson]
q:56 [in RegLang.regexp]
q:57 [in RegLang.two_way]
q:60 [in RegLang.two_way]
q:62 [in RegLang.two_way]
q:63 [in RegLang.nfa]
q:64 [in RegLang.regexp]
q:65 [in RegLang.two_way]
q:66 [in RegLang.wmso]
q:66 [in RegLang.shepherdson]
q:69 [in RegLang.nfa]
q:72 [in RegLang.wmso]
q:73 [in RegLang.nfa]
q:75 [in RegLang.regexp]
q:75 [in RegLang.nfa]
q:78 [in RegLang.shepherdson]
q:8 [in RegLang.vardi]
q:81 [in RegLang.regexp]
q:81 [in RegLang.nfa]
q:82 [in RegLang.misc]
q:82 [in RegLang.shepherdson]
q:85 [in RegLang.wmso]
q:85 [in RegLang.shepherdson]
q:86 [in RegLang.nfa]
q:87 [in RegLang.shepherdson]
q:88 [in RegLang.shepherdson]
q:91 [in RegLang.wmso]
q:94 [in RegLang.wmso]
q:99 [in RegLang.shepherdson]
R
rT:152 [in RegLang.misc]rT:156 [in RegLang.misc]
r:127 [in RegLang.nfa]
r:130 [in RegLang.nfa]
r:132 [in RegLang.nfa]
r:136 [in RegLang.nfa]
r:139 [in RegLang.nfa]
r:142 [in RegLang.nfa]
r:144 [in RegLang.shepherdson]
r:147 [in RegLang.nfa]
r:15 [in RegLang.regexp]
r:157 [in RegLang.regexp]
r:160 [in RegLang.regexp]
r:164 [in RegLang.regexp]
r:166 [in RegLang.regexp]
r:35 [in RegLang.regexp]
r:40 [in RegLang.languages]
r:41 [in RegLang.regexp]
r:44 [in RegLang.regexp]
r:46 [in RegLang.regexp]
r:48 [in RegLang.regexp]
r:50 [in RegLang.regexp]
S
Sf:165 [in RegLang.misc]Sf:170 [in RegLang.misc]
ss:38 [in RegLang.misc]
ss:41 [in RegLang.misc]
sT:106 [in RegLang.misc]
s:12 [in RegLang.wmso]
s:135 [in RegLang.nfa]
s:137 [in RegLang.wmso]
s:146 [in RegLang.nfa]
s:148 [in RegLang.wmso]
s:15 [in RegLang.nfa]
s:156 [in RegLang.wmso]
s:158 [in RegLang.regexp]
s:161 [in RegLang.regexp]
s:162 [in RegLang.wmso]
s:18 [in RegLang.wmso]
s:196 [in RegLang.dfa]
s:198 [in RegLang.dfa]
s:199 [in RegLang.wmso]
s:211 [in RegLang.wmso]
s:213 [in RegLang.wmso]
s:214 [in RegLang.wmso]
s:217 [in RegLang.wmso]
s:219 [in RegLang.wmso]
s:221 [in RegLang.wmso]
s:222 [in RegLang.wmso]
s:224 [in RegLang.wmso]
s:226 [in RegLang.wmso]
s:229 [in RegLang.wmso]
s:23 [in RegLang.misc]
s:231 [in RegLang.wmso]
s:234 [in RegLang.wmso]
s:236 [in RegLang.wmso]
s:239 [in RegLang.wmso]
s:241 [in RegLang.wmso]
s:243 [in RegLang.wmso]
s:245 [in RegLang.wmso]
s:26 [in RegLang.misc]
s:262 [in RegLang.wmso]
s:268 [in RegLang.wmso]
s:275 [in RegLang.wmso]
s:280 [in RegLang.wmso]
s:282 [in RegLang.wmso]
s:284 [in RegLang.wmso]
s:286 [in RegLang.wmso]
s:30 [in RegLang.misc]
s:31 [in RegLang.wmso]
s:323 [in RegLang.wmso]
s:325 [in RegLang.wmso]
s:33 [in RegLang.nfa]
s:34 [in RegLang.nfa]
s:35 [in RegLang.wmso]
s:36 [in RegLang.misc]
s:39 [in RegLang.misc]
s:41 [in RegLang.languages]
s:44 [in RegLang.misc]
s:49 [in RegLang.regexp]
s:49 [in RegLang.two_way]
s:50 [in RegLang.misc]
s:51 [in RegLang.regexp]
s:52 [in RegLang.wmso]
s:54 [in RegLang.wmso]
s:55 [in RegLang.dfa]
s:56 [in RegLang.wmso]
s:60 [in RegLang.misc]
s:65 [in RegLang.misc]
s:72 [in RegLang.misc]
s:94 [in RegLang.dfa]
s:96 [in RegLang.wmso]
T
T':160 [in RegLang.misc]T':91 [in RegLang.misc]
T1:10 [in RegLang.misc]
T1:12 [in RegLang.misc]
T1:6 [in RegLang.misc]
T2:11 [in RegLang.misc]
T2:13 [in RegLang.misc]
T2:7 [in RegLang.misc]
T:1 [in RegLang.wmso]
T:10 [in RegLang.shepherdson]
T:103 [in RegLang.misc]
T:104 [in RegLang.misc]
T:111 [in RegLang.misc]
T:114 [in RegLang.misc]
T:13 [in RegLang.regexp]
T:148 [in RegLang.misc]
T:159 [in RegLang.misc]
T:16 [in RegLang.vardi]
T:193 [in RegLang.dfa]
T:197 [in RegLang.dfa]
T:20 [in RegLang.misc]
T:21 [in RegLang.regexp]
t:227 [in RegLang.wmso]
t:232 [in RegLang.wmso]
t:235 [in RegLang.wmso]
t:237 [in RegLang.wmso]
t:240 [in RegLang.wmso]
t:242 [in RegLang.wmso]
T:25 [in RegLang.misc]
T:261 [in RegLang.wmso]
T:267 [in RegLang.wmso]
T:274 [in RegLang.wmso]
T:29 [in RegLang.misc]
t:3 [in RegLang.wmso]
T:33 [in RegLang.regexp]
T:33 [in RegLang.misc]
T:33 [in RegLang.vardi]
T:37 [in RegLang.misc]
T:4 [in RegLang.vardi]
T:40 [in RegLang.misc]
T:42 [in RegLang.misc]
T:43 [in RegLang.two_way]
T:48 [in RegLang.misc]
T:5 [in RegLang.shepherdson]
T:53 [in RegLang.dfa]
T:58 [in RegLang.misc]
T:64 [in RegLang.misc]
T:74 [in RegLang.misc]
T:77 [in RegLang.misc]
T:80 [in RegLang.misc]
T:85 [in RegLang.misc]
T:90 [in RegLang.misc]
T:96 [in RegLang.misc]
U
u:13 [in RegLang.myhill_nerode]u:165 [in RegLang.wmso]
u:170 [in RegLang.wmso]
u:171 [in RegLang.wmso]
u:172 [in RegLang.wmso]
u:209 [in RegLang.dfa]
u:219 [in RegLang.dfa]
u:38 [in RegLang.myhill_nerode]
u:7 [in RegLang.myhill_nerode]
V
vs:139 [in RegLang.wmso]vv:19 [in RegLang.languages]
vv:58 [in RegLang.languages]
vv:59 [in RegLang.languages]
vv:64 [in RegLang.languages]
v1:180 [in RegLang.wmso]
v1:184 [in RegLang.wmso]
v2:181 [in RegLang.wmso]
v2:185 [in RegLang.wmso]
v:105 [in RegLang.wmso]
v:11 [in RegLang.languages]
v:118 [in RegLang.wmso]
v:121 [in RegLang.wmso]
v:126 [in RegLang.wmso]
v:129 [in RegLang.wmso]
v:13 [in RegLang.languages]
v:135 [in RegLang.wmso]
v:14 [in RegLang.myhill_nerode]
v:150 [in RegLang.wmso]
v:154 [in RegLang.wmso]
v:164 [in RegLang.wmso]
v:169 [in RegLang.wmso]
v:175 [in RegLang.wmso]
v:179 [in RegLang.wmso]
v:181 [in RegLang.regexp]
v:187 [in RegLang.wmso]
v:193 [in RegLang.wmso]
v:198 [in RegLang.wmso]
v:210 [in RegLang.dfa]
v:220 [in RegLang.dfa]
v:34 [in RegLang.languages]
v:37 [in RegLang.languages]
v:39 [in RegLang.wmso]
v:39 [in RegLang.myhill_nerode]
v:53 [in RegLang.wmso]
v:57 [in RegLang.languages]
v:6 [in RegLang.languages]
v:65 [in RegLang.languages]
v:65 [in RegLang.wmso]
v:8 [in RegLang.myhill_nerode]
v:81 [in RegLang.wmso]
v:90 [in RegLang.wmso]
W
w1:105 [in RegLang.regexp]w1:14 [in RegLang.languages]
w1:46 [in RegLang.languages]
w1:48 [in RegLang.languages]
w1:60 [in RegLang.languages]
w1:84 [in RegLang.regexp]
w1:93 [in RegLang.regexp]
w1:99 [in RegLang.regexp]
w2:100 [in RegLang.regexp]
w2:106 [in RegLang.regexp]
w2:15 [in RegLang.languages]
w2:47 [in RegLang.languages]
w2:49 [in RegLang.languages]
w2:61 [in RegLang.languages]
w2:85 [in RegLang.regexp]
w2:94 [in RegLang.regexp]
w:10 [in RegLang.languages]
w:101 [in RegLang.wmso]
w:109 [in RegLang.regexp]
w:109 [in RegLang.wmso]
w:112 [in RegLang.wmso]
w:119 [in RegLang.regexp]
w:124 [in RegLang.regexp]
w:133 [in RegLang.shepherdson]
w:14 [in RegLang.nfa]
w:151 [in RegLang.nfa]
w:158 [in RegLang.wmso]
w:16 [in RegLang.regexp]
w:162 [in RegLang.regexp]
w:167 [in RegLang.regexp]
w:168 [in RegLang.dfa]
w:169 [in RegLang.regexp]
w:17 [in RegLang.languages]
w:172 [in RegLang.regexp]
w:184 [in RegLang.dfa]
w:193 [in RegLang.regexp]
w:20 [in RegLang.dfa]
w:211 [in RegLang.dfa]
w:22 [in RegLang.shepherdson]
w:221 [in RegLang.dfa]
w:24 [in RegLang.regexp]
w:25 [in RegLang.dfa]
w:25 [in RegLang.languages]
w:25 [in RegLang.minimization]
w:27 [in RegLang.minimization]
w:28 [in RegLang.languages]
w:31 [in RegLang.languages]
w:334 [in RegLang.wmso]
w:35 [in RegLang.dfa]
w:368 [in RegLang.wmso]
w:39 [in RegLang.dfa]
w:40 [in RegLang.myhill_nerode]
w:42 [in RegLang.languages]
w:42 [in RegLang.wmso]
w:43 [in RegLang.dfa]
w:45 [in RegLang.languages]
w:47 [in RegLang.wmso]
w:5 [in RegLang.minimization]
w:50 [in RegLang.wmso]
w:55 [in RegLang.wmso]
w:58 [in RegLang.two_way]
w:61 [in RegLang.regexp]
w:63 [in RegLang.minimization]
w:7 [in RegLang.languages]
w:76 [in RegLang.regexp]
w:80 [in RegLang.wmso]
w:83 [in RegLang.regexp]
w:9 [in RegLang.nfa]
X
xi:119 [in RegLang.shepherdson]xj:120 [in RegLang.shepherdson]
xk:118 [in RegLang.shepherdson]
x0:21 [in RegLang.misc]
x1:107 [in RegLang.nfa]
x1:116 [in RegLang.nfa]
x1:93 [in RegLang.nfa]
x1:98 [in RegLang.nfa]
x2:108 [in RegLang.nfa]
x2:117 [in RegLang.nfa]
x2:94 [in RegLang.nfa]
x2:99 [in RegLang.nfa]
x:1 [in RegLang.misc]
X:10 [in RegLang.myhill_nerode]
x:100 [in RegLang.nfa]
X:101 [in RegLang.regexp]
x:101 [in RegLang.shepherdson]
x:102 [in RegLang.regexp]
X:107 [in RegLang.regexp]
x:107 [in RegLang.misc]
x:11 [in RegLang.setoid_leq]
x:11 [in RegLang.shepherdson]
X:110 [in RegLang.regexp]
x:110 [in RegLang.nfa]
x:110 [in RegLang.shepherdson]
x:111 [in RegLang.regexp]
x:112 [in RegLang.nfa]
x:113 [in RegLang.misc]
x:114 [in RegLang.dfa]
x:114 [in RegLang.regexp]
x:114 [in RegLang.nfa]
x:115 [in RegLang.misc]
x:117 [in RegLang.regexp]
x:118 [in RegLang.nfa]
x:12 [in RegLang.vardi]
x:122 [in RegLang.regexp]
x:124 [in RegLang.dfa]
x:124 [in RegLang.shepherdson]
x:125 [in RegLang.regexp]
x:126 [in RegLang.nfa]
x:128 [in RegLang.nfa]
X:129 [in RegLang.regexp]
x:130 [in RegLang.regexp]
x:130 [in RegLang.misc]
x:131 [in RegLang.nfa]
x:132 [in RegLang.misc]
x:134 [in RegLang.dfa]
X:134 [in RegLang.regexp]
x:134 [in RegLang.nfa]
x:135 [in RegLang.regexp]
x:135 [in RegLang.misc]
x:135 [in RegLang.shepherdson]
x:137 [in RegLang.nfa]
x:138 [in RegLang.shepherdson]
x:139 [in RegLang.misc]
x:14 [in RegLang.dfa]
X:14 [in RegLang.misc]
x:140 [in RegLang.nfa]
x:141 [in RegLang.regexp]
x:141 [in RegLang.shepherdson]
x:142 [in RegLang.regexp]
x:142 [in RegLang.misc]
x:145 [in RegLang.dfa]
x:145 [in RegLang.nfa]
x:145 [in RegLang.shepherdson]
x:146 [in RegLang.dfa]
x:146 [in RegLang.misc]
x:146 [in RegLang.shepherdson]
x:148 [in RegLang.regexp]
x:15 [in RegLang.minimization]
x:15 [in RegLang.wmso]
x:15 [in RegLang.vardi]
x:154 [in RegLang.dfa]
x:154 [in RegLang.nfa]
x:155 [in RegLang.regexp]
x:155 [in RegLang.misc]
x:159 [in RegLang.dfa]
x:16 [in RegLang.dfa]
X:162 [in RegLang.misc]
X:166 [in RegLang.wmso]
X:167 [in RegLang.misc]
x:17 [in RegLang.misc]
x:17 [in RegLang.minimization]
x:171 [in RegLang.misc]
x:174 [in RegLang.dfa]
X:174 [in RegLang.wmso]
X:176 [in RegLang.wmso]
x:18 [in RegLang.misc]
x:18 [in RegLang.shepherdson]
X:188 [in RegLang.wmso]
x:19 [in RegLang.dfa]
x:19 [in RegLang.regexp]
X:190 [in RegLang.wmso]
x:196 [in RegLang.regexp]
x:20 [in RegLang.regexp]
X:202 [in RegLang.wmso]
x:203 [in RegLang.dfa]
x:206 [in RegLang.dfa]
X:207 [in RegLang.wmso]
x:21 [in RegLang.dfa]
x:21 [in RegLang.languages]
x:216 [in RegLang.dfa]
x:22 [in RegLang.misc]
x:23 [in RegLang.dfa]
x:23 [in RegLang.shepherdson]
X:24 [in RegLang.wmso]
x:24 [in RegLang.shepherdson]
X:247 [in RegLang.wmso]
X:249 [in RegLang.wmso]
X:251 [in RegLang.wmso]
X:253 [in RegLang.wmso]
X:255 [in RegLang.wmso]
x:26 [in RegLang.dfa]
x:26 [in RegLang.minimization]
x:263 [in RegLang.wmso]
X:27 [in RegLang.vardi]
x:271 [in RegLang.wmso]
x:272 [in RegLang.wmso]
x:279 [in RegLang.wmso]
x:28 [in RegLang.nfa]
x:28 [in RegLang.minimization]
x:28 [in RegLang.shepherdson]
x:288 [in RegLang.wmso]
x:29 [in RegLang.dfa]
x:29 [in RegLang.languages]
X:291 [in RegLang.wmso]
X:294 [in RegLang.wmso]
x:295 [in RegLang.wmso]
X:298 [in RegLang.wmso]
x:3 [in RegLang.minimization]
x:3 [in RegLang.vardi]
X:30 [in RegLang.vardi]
x:30 [in RegLang.myhill_nerode]
X:300 [in RegLang.wmso]
X:301 [in RegLang.wmso]
X:304 [in RegLang.wmso]
x:305 [in RegLang.wmso]
x:31 [in RegLang.nfa]
X:31 [in RegLang.vardi]
x:310 [in RegLang.wmso]
X:314 [in RegLang.wmso]
X:318 [in RegLang.wmso]
x:32 [in RegLang.dfa]
x:32 [in RegLang.nfa]
x:32 [in RegLang.vardi]
x:32 [in RegLang.myhill_nerode]
X:336 [in RegLang.wmso]
x:338 [in RegLang.wmso]
x:34 [in RegLang.dfa]
x:34 [in RegLang.minimization]
x:34 [in RegLang.shepherdson]
X:340 [in RegLang.wmso]
X:345 [in RegLang.wmso]
x:346 [in RegLang.wmso]
x:35 [in RegLang.minimization]
X:35 [in RegLang.myhill_nerode]
x:36 [in RegLang.minimization]
X:36 [in RegLang.wmso]
X:361 [in RegLang.wmso]
x:38 [in RegLang.minimization]
x:39 [in RegLang.nfa]
x:39 [in RegLang.shepherdson]
x:40 [in RegLang.dfa]
x:40 [in RegLang.minimization]
X:40 [in RegLang.wmso]
x:43 [in RegLang.shepherdson]
x:44 [in RegLang.minimization]
X:44 [in RegLang.wmso]
x:45 [in RegLang.nfa]
x:45 [in RegLang.two_way]
x:46 [in RegLang.dfa]
x:46 [in RegLang.two_way]
x:47 [in RegLang.minimization]
x:49 [in RegLang.dfa]
x:49 [in RegLang.nfa]
X:5 [in RegLang.myhill_nerode]
x:50 [in RegLang.two_way]
X:51 [in RegLang.nfa]
x:51 [in RegLang.shepherdson]
x:52 [in RegLang.dfa]
x:52 [in RegLang.misc]
x:53 [in RegLang.misc]
X:54 [in RegLang.regexp]
x:54 [in RegLang.misc]
X:55 [in RegLang.nfa]
x:55 [in RegLang.misc]
x:55 [in RegLang.minimization]
x:56 [in RegLang.dfa]
x:57 [in RegLang.regexp]
x:57 [in RegLang.nfa]
x:57 [in RegLang.minimization]
x:59 [in RegLang.regexp]
x:59 [in RegLang.minimization]
x:6 [in RegLang.shepherdson]
x:60 [in RegLang.dfa]
x:61 [in RegLang.dfa]
x:61 [in RegLang.minimization]
X:62 [in RegLang.regexp]
x:62 [in RegLang.minimization]
X:62 [in RegLang.wmso]
x:62 [in RegLang.shepherdson]
x:64 [in RegLang.minimization]
x:65 [in RegLang.regexp]
x:67 [in RegLang.dfa]
X:67 [in RegLang.regexp]
x:68 [in RegLang.regexp]
X:68 [in RegLang.wmso]
x:69 [in RegLang.shepherdson]
x:71 [in RegLang.dfa]
X:71 [in RegLang.regexp]
x:72 [in RegLang.regexp]
x:74 [in RegLang.dfa]
x:75 [in RegLang.misc]
X:77 [in RegLang.wmso]
x:78 [in RegLang.misc]
x:79 [in RegLang.dfa]
X:79 [in RegLang.regexp]
x:8 [in RegLang.nfa]
x:8 [in RegLang.minimization]
x:81 [in RegLang.dfa]
x:83 [in RegLang.misc]
x:84 [in RegLang.dfa]
x:84 [in RegLang.misc]
x:86 [in RegLang.dfa]
x:88 [in RegLang.dfa]
x:88 [in RegLang.misc]
x:89 [in RegLang.dfa]
X:89 [in RegLang.regexp]
x:89 [in RegLang.misc]
x:9 [in RegLang.dfa]
x:9 [in RegLang.setoid_leq]
x:9 [in RegLang.vardi]
x:90 [in RegLang.regexp]
x:91 [in RegLang.dfa]
x:91 [in RegLang.nfa]
X:93 [in RegLang.misc]
x:95 [in RegLang.dfa]
X:95 [in RegLang.regexp]
x:96 [in RegLang.dfa]
x:96 [in RegLang.regexp]
x:96 [in RegLang.nfa]
x:97 [in RegLang.dfa]
x:98 [in RegLang.dfa]
x:98 [in RegLang.misc]
Y
yi:122 [in RegLang.shepherdson]yj:123 [in RegLang.shepherdson]
yk:121 [in RegLang.shepherdson]
y:10 [in RegLang.setoid_leq]
y:102 [in RegLang.shepherdson]
y:103 [in RegLang.regexp]
y:108 [in RegLang.misc]
y:111 [in RegLang.shepherdson]
y:112 [in RegLang.regexp]
y:115 [in RegLang.regexp]
y:118 [in RegLang.regexp]
y:12 [in RegLang.nfa]
y:12 [in RegLang.setoid_leq]
y:123 [in RegLang.regexp]
y:125 [in RegLang.dfa]
y:126 [in RegLang.dfa]
y:126 [in RegLang.regexp]
y:130 [in RegLang.dfa]
y:131 [in RegLang.dfa]
y:131 [in RegLang.regexp]
y:131 [in RegLang.misc]
y:133 [in RegLang.misc]
y:136 [in RegLang.regexp]
y:136 [in RegLang.misc]
y:139 [in RegLang.dfa]
y:140 [in RegLang.dfa]
y:140 [in RegLang.misc]
y:143 [in RegLang.regexp]
y:144 [in RegLang.dfa]
y:144 [in RegLang.misc]
y:147 [in RegLang.misc]
y:150 [in RegLang.dfa]
y:151 [in RegLang.dfa]
y:154 [in RegLang.misc]
y:155 [in RegLang.dfa]
y:16 [in RegLang.wmso]
Y:163 [in RegLang.misc]
y:166 [in RegLang.misc]
Y:167 [in RegLang.wmso]
Y:168 [in RegLang.misc]
y:17 [in RegLang.dfa]
y:175 [in RegLang.dfa]
Y:177 [in RegLang.wmso]
y:19 [in RegLang.misc]
Y:191 [in RegLang.wmso]
y:207 [in RegLang.dfa]
y:217 [in RegLang.dfa]
y:289 [in RegLang.wmso]
Y:29 [in RegLang.vardi]
Y:292 [in RegLang.wmso]
Y:296 [in RegLang.wmso]
y:297 [in RegLang.wmso]
Y:302 [in RegLang.wmso]
Y:306 [in RegLang.wmso]
y:307 [in RegLang.wmso]
y:4 [in RegLang.minimization]
y:48 [in RegLang.minimization]
y:58 [in RegLang.minimization]
y:59 [in RegLang.nfa]
y:60 [in RegLang.regexp]
Y:63 [in RegLang.wmso]
y:68 [in RegLang.dfa]
y:69 [in RegLang.regexp]
Y:69 [in RegLang.wmso]
y:72 [in RegLang.dfa]
y:73 [in RegLang.regexp]
y:76 [in RegLang.misc]
Y:78 [in RegLang.wmso]
y:9 [in RegLang.minimization]
y:91 [in RegLang.regexp]
y:92 [in RegLang.dfa]
Y:94 [in RegLang.misc]
y:97 [in RegLang.regexp]
Z
z:103 [in RegLang.shepherdson]z:104 [in RegLang.regexp]
z:108 [in RegLang.regexp]
z:112 [in RegLang.shepherdson]
z:113 [in RegLang.regexp]
z:12 [in RegLang.shepherdson]
z:134 [in RegLang.misc]
z:137 [in RegLang.regexp]
z:137 [in RegLang.misc]
z:138 [in RegLang.regexp]
z:139 [in RegLang.regexp]
z:140 [in RegLang.regexp]
z:143 [in RegLang.misc]
z:208 [in RegLang.dfa]
z:218 [in RegLang.dfa]
z:7 [in RegLang.shepherdson]
z:70 [in RegLang.regexp]
z:70 [in RegLang.shepherdson]
z:73 [in RegLang.dfa]
z:82 [in RegLang.regexp]
z:92 [in RegLang.regexp]
z:98 [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_nseq_eq [in RegLang.dfa]
cat_size [in RegLang.wmso]
cat_beyond [in RegLang.wmso]
cat_prefix [in RegLang.wmso]
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]
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_to_re_size [in RegLang.regexp]
dfa_to_re_correct [in RegLang.regexp]
dfa_L [in RegLang.regexp]
dfa_to_nfa_correct [in RegLang.nfa]
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_cf_size [in RegLang.myhill_nerode]
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_sub [in RegLang.misc]
functional_srel [in RegLang.shepherdson]
H
h_flatten [in RegLang.languages]h_seq [in RegLang.languages]
h0 [in RegLang.languages]
I
image_fun_proof [in RegLang.dfa]image_ext [in RegLang.languages]
image_refines [in RegLang.shepherdson]
image_rc [in RegLang.shepherdson]
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_max [in RegLang.misc]
inord_inj [in RegLang.shepherdson]
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_R0 [in RegLang.regexp]
mem_I_of [in RegLang.wmso]
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_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]
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]
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_cons [in RegLang.misc]
nth_glueS [in RegLang.wmso]
nth_glue0 [in RegLang.wmso]
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_correct [in RegLang.regexp]
rev_flatten [in RegLang.misc]
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_induction [in RegLang.misc]
size_glue [in RegLang.wmso]
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_uniq [in RegLang.misc]
term_srel [in RegLang.shepherdson]
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]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]
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]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.nfa]
word [in RegLang.minimization]
word [in RegLang.myhill_nerode]
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]
collb_equiv [in RegLang.minimization]
coll_fun [in RegLang.minimization]
comp [in RegLang.vardi]
compl [in RegLang.languages]
compL [in RegLang.vardi]
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_to_re [in RegLang.regexp]
dfa_to_nfa [in RegLang.nfa]
dfa_prune [in RegLang.minimization]
dfa_iso [in RegLang.minimization]
dfa_to_mg [in RegLang.myhill_nerode]
dfa_to_cf [in RegLang.myhill_nerode]
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_star [in RegLang.nfa]
enfa_conc [in RegLang.nfa]
enfa_lang [in RegLang.nfa]
enfa_for_ltn [in RegLang.wmso]
eps [in RegLang.languages]
eps_reach [in RegLang.nfa]
exn [in RegLang.wmso]
exseqb [in RegLang.dfa]
Ex1 [in RegLang.wmso]
F
form_eqType [in RegLang.regexp]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.regexp]L [in RegLang.two_way]
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]
min_subFinType [in RegLang.minimization]
min_finType [in RegLang.minimization]
min_choiceType [in RegLang.minimization]
min_eqType [in RegLang.minimization]
min_subType [in RegLang.minimization]
min_quotType [in RegLang.minimization]
mso_lang [in RegLang.wmso]
N
Neg [in RegLang.regexp]nerode [in RegLang.myhill_nerode]
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]
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]
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.regexp]R [in RegLang.two_way]
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_predType [in RegLang.regexp]
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]word_eqType [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 | (2159 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) |
| Binder 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 | (1392 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 | (323 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) |
| 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) |
| 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) |
| 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 | (191 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) |