| 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 | (489 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 | (5 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (27 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 | (13 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 | (263 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 | (29 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 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 | (18 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 | (71 entries) |
Global Index
A
and_dec [instance, in CFG.Base]app_equi_proper [instance, in CFG.Base]
app_incl_proper [instance, in CFG.Base]
B
Base [library]bin [definition, in CFG.Binarize]
Binarize [library]
binary [definition, in CFG.Binarize]
binary_unit [lemma, in CFG.Chomsky]
binary_elimE [lemma, in CFG.Chomsky]
binary_sep [lemma, in CFG.Chomsky]
bin_language [lemma, in CFG.Binarize]
bin_der_equiv [lemma, in CFG.Binarize]
bin_binary [lemma, in CFG.Binarize]
bin_dom [lemma, in CFG.Chomsky]
bool_eq_dec [instance, in CFG.Base]
C
card [definition, in CFG.Base]Cardinality [section, in CFG.Base]
Cardinality.X [variable, in CFG.Base]
card_equi_proper [instance, in CFG.Base]
card_or [lemma, in CFG.Base]
card_lt [lemma, in CFG.Base]
card_equi [lemma, in CFG.Base]
card_ex [lemma, in CFG.Base]
card_0 [lemma, in CFG.Base]
card_cons_rem [lemma, in CFG.Base]
card_eq [lemma, in CFG.Base]
card_le [lemma, in CFG.Base]
card_not_in_rem [lemma, in CFG.Base]
card_in_rem [lemma, in CFG.Base]
charfree [definition, in CFG.Separate]
chomsky [definition, in CFG.Chomsky]
Chomsky [library]
chomsky_normalform [lemma, in CFG.Chomsky]
closure [definition, in CFG.ElimE]
closure_slist [lemma, in CFG.ElimE]
concat [definition, in CFG.Lists]
concat_split [lemma, in CFG.Lists]
cons_equi_proper [instance, in CFG.Base]
cons_incl_proper [instance, in CFG.Base]
count_decr [lemma, in CFG.Binarize]
count_bin [definition, in CFG.Binarize]
count_decr [lemma, in CFG.Separate]
count_sep_decr [lemma, in CFG.Separate]
count_chars_decr [lemma, in CFG.Separate]
count_chars_split [lemma, in CFG.Separate]
count_sep_substL [lemma, in CFG.Separate]
count_chars_substL [lemma, in CFG.Separate]
count_sep_split [lemma, in CFG.Separate]
count_sep [definition, in CFG.Separate]
count_chars [definition, in CFG.Separate]
D
dec [definition, in CFG.Base]decision [definition, in CFG.Base]
dec_charfree [instance, in CFG.Separate]
dec_prop_iff [lemma, in CFG.Base]
dec_DM_impl [lemma, in CFG.Base]
dec_DM_and [lemma, in CFG.Base]
dec_DN [lemma, in CFG.Base]
Dec_Emptys.G [variable, in CFG.Dec_Empty]
Dec_Emptys [section, in CFG.Dec_Empty]
Dec_Word.u [variable, in CFG.Dec_Word]
Dec_Word.G [variable, in CFG.Dec_Word]
Dec_Word [section, in CFG.Dec_Word]
Dec_Word [library]
Dec_Empty [library]
Definitions [library]
delE [definition, in CFG.ElimE]
DelE [section, in CFG.ElimE]
delE_der_equiv [lemma, in CFG.ElimE]
delE_rules [lemma, in CFG.ElimE]
delE_preserveG [lemma, in CFG.ElimE]
delE_efree [lemma, in CFG.ElimE]
DelE.G [variable, in CFG.ElimE]
der [inductive, in CFG.Derivation]
derE_nullable [lemma, in CFG.ElimE]
derf [inductive, in CFG.Derivation]
derfelimU_derfG [lemma, in CFG.ElimU]
derfG_derfelimU [lemma, in CFG.ElimU]
derf_der_equiv [lemma, in CFG.Derivation]
derf_derT [lemma, in CFG.Derivation]
derf_trans [lemma, in CFG.Derivation]
derf_split [lemma, in CFG.Derivation]
derf_concat [lemma, in CFG.Derivation]
derf_productive [lemma, in CFG.Dec_Empty]
derf_DW [lemma, in CFG.Dec_Word]
derI [inductive, in CFG.Derivation]
derIRefl [constructor, in CFG.Derivation]
derIRule [constructor, in CFG.Derivation]
derITrans [constructor, in CFG.Derivation]
Derivation [library]
derI_derf [lemma, in CFG.Derivation]
derL [inductive, in CFG.Derivation]
derL_der_equiv [lemma, in CFG.Derivation]
derT [inductive, in CFG.Derivation]
derTRefl [constructor, in CFG.Derivation]
derTRule [constructor, in CFG.Derivation]
derTTrans [constructor, in CFG.Derivation]
derT_concat [lemma, in CFG.Derivation]
derT_trans [lemma, in CFG.Derivation]
derT_derI [lemma, in CFG.Derivation]
derT_der_equiv [lemma, in CFG.Derivation]
derT_slist [lemma, in CFG.ElimE]
der_equiv_G [lemma, in CFG.Derivation]
der_subset [lemma, in CFG.Derivation]
der_G_inlL [lemma, in CFG.Inlining]
der_inlL_G [lemma, in CFG.Inlining]
der_inlL_G' [lemma, in CFG.Inlining]
der_substG_G_equiv [lemma, in CFG.Inlining]
der_G_substG [lemma, in CFG.Inlining]
der_G_substG' [lemma, in CFG.Inlining]
der_substG_G [lemma, in CFG.Inlining]
der_dec [instance, in CFG.Dec_Word]
der_G_delE [lemma, in CFG.ElimE]
der_eclosure_equiv [lemma, in CFG.ElimE]
disjoint [definition, in CFG.Base]
disjoint_cons [lemma, in CFG.Base]
disjoint_forall [lemma, in CFG.Base]
disjoint_incl [lemma, in CFG.Base]
disjoint_symm [lemma, in CFG.Base]
disjoint_nil' [lemma, in CFG.Base]
disjoint_nil [lemma, in CFG.Base]
dom [definition, in CFG.Symbols]
domG_rule [lemma, in CFG.Symbols]
domV [definition, in CFG.ElimU]
domVG_rule [lemma, in CFG.ElimU]
dom_domV [lemma, in CFG.ElimU]
dom_subset [lemma, in CFG.Symbols]
Dupfree [section, in CFG.Base]
dupfree [inductive, in CFG.Base]
dupfreeC [constructor, in CFG.Base]
dupfreeN [constructor, in CFG.Base]
dupfree_inv [definition, in CFG.Base]
dupfree_in_power [lemma, in CFG.Base]
dupfree_power [lemma, in CFG.Base]
dupfree_undup [lemma, in CFG.Base]
dupfree_card [lemma, in CFG.Base]
dupfree_dec [lemma, in CFG.Base]
dupfree_filter [lemma, in CFG.Base]
dupfree_map [lemma, in CFG.Base]
dupfree_app [lemma, in CFG.Base]
dupfree_cons [lemma, in CFG.Base]
Dupfree.X [variable, in CFG.Base]
DW [definition, in CFG.Dec_Word]
DW_der_equiv [lemma, in CFG.Dec_Word]
DW_der_equiv' [lemma, in CFG.Dec_Word]
DW_derf' [lemma, in CFG.Dec_Word]
E
eclosed [definition, in CFG.ElimE]eclosed_eclosure [lemma, in CFG.ElimE]
eclosure [definition, in CFG.ElimE]
EClosure [section, in CFG.ElimE]
eclosure_der [lemma, in CFG.ElimE]
EClosure.G [variable, in CFG.ElimE]
efree [definition, in CFG.ElimE]
efree_unit [lemma, in CFG.Chomsky]
efree_elimE [lemma, in CFG.ElimE]
elimE [definition, in CFG.ElimE]
ElimE [library]
elimE_language [lemma, in CFG.ElimE]
elimU [definition, in CFG.ElimU]
ElimU [library]
elimU_der_equiv [lemma, in CFG.ElimU]
elimU_corr3 [lemma, in CFG.ElimU]
elimU_corr3' [lemma, in CFG.ElimU]
elimU_corr2 [lemma, in CFG.ElimU]
elimU_corr [lemma, in CFG.ElimU]
Equi [section, in CFG.Base]
equi [definition, in CFG.Base]
equi_rotate [lemma, in CFG.Base]
equi_shift [lemma, in CFG.Base]
equi_swap [lemma, in CFG.Base]
equi_dup [lemma, in CFG.Base]
equi_push [lemma, in CFG.Base]
equi_Equivalence [instance, in CFG.Base]
Equi.X [variable, in CFG.Base]
eq_dec_prod [instance, in CFG.Lists]
excluded_unit [lemma, in CFG.Chomsky]
excluded_free [lemma, in CFG.Chomsky]
exists_phrase_dec [instance, in CFG.Definitions]
exists_rule_dec [instance, in CFG.Definitions]
exists_dec [instance, in CFG.Dec_Empty]
F
False_dec [instance, in CFG.Base]FCI [module, in CFG.Base]
FCI.C [definition, in CFG.Base]
FCI.closure [lemma, in CFG.Base]
FCI.F [definition, in CFG.Base]
FCI.FCI [section, in CFG.Base]
FCI.FCI.step [variable, in CFG.Base]
FCI.FCI.V [variable, in CFG.Base]
FCI.FCI.X [variable, in CFG.Base]
FCI.fp [lemma, in CFG.Base]
FCI.incl [lemma, in CFG.Base]
FCI.ind [lemma, in CFG.Base]
FCI.it_incl [lemma, in CFG.Base]
FCI.pick [lemma, in CFG.Base]
fCons [constructor, in CFG.Derivation]
filter [definition, in CFG.Base]
FilterComm [section, in CFG.Base]
FilterComm.p [variable, in CFG.Base]
FilterComm.q [variable, in CFG.Base]
FilterComm.X [variable, in CFG.Base]
FilterLemmas [section, in CFG.Base]
FilterLemmas_pq.q [variable, in CFG.Base]
FilterLemmas_pq.p [variable, in CFG.Base]
FilterLemmas_pq.X [variable, in CFG.Base]
FilterLemmas_pq [section, in CFG.Base]
FilterLemmas.p [variable, in CFG.Base]
FilterLemmas.X [variable, in CFG.Base]
filter_rule_dec [instance, in CFG.Definitions]
filter_comm [lemma, in CFG.Base]
filter_and [lemma, in CFG.Base]
filter_pq_eq [lemma, in CFG.Base]
filter_pq_mono [lemma, in CFG.Base]
filter_fst' [lemma, in CFG.Base]
filter_fst [lemma, in CFG.Base]
filter_app [lemma, in CFG.Base]
filter_id [lemma, in CFG.Base]
filter_mono [lemma, in CFG.Base]
filter_incl [lemma, in CFG.Base]
filter_prod_dec [instance, in CFG.Lists]
FP [definition, in CFG.Base]
fp_binary [lemma, in CFG.Binarize]
fp_bin [lemma, in CFG.Binarize]
fp_uniform [lemma, in CFG.Separate]
fp_sep [lemma, in CFG.Separate]
fRefl [constructor, in CFG.Derivation]
fresh [definition, in CFG.Symbols]
fresh_symbs [lemma, in CFG.Symbols]
fRule [constructor, in CFG.Derivation]
fsts [definition, in CFG.Lists]
fsts_split [lemma, in CFG.Lists]
fsts_comb_corr [lemma, in CFG.Dec_Word]
fsts_comb_corr2 [lemma, in CFG.Dec_Word]
fsts_comb_corr1 [lemma, in CFG.Dec_Word]
fsts_comb [definition, in CFG.Dec_Word]
G
gDer [constructor, in CFG.Derivation]getNat [definition, in CFG.Symbols]
grammar [definition, in CFG.Definitions]
I
iff_dec [instance, in CFG.Base]impl_dec [instance, in CFG.Base]
inclp [definition, in CFG.Base]
Inclusion [section, in CFG.Base]
Inclusion.X [variable, in CFG.Base]
incl_equi_proper [instance, in CFG.Base]
incl_preorder [instance, in CFG.Base]
incl_app_left [lemma, in CFG.Base]
incl_lrcons [lemma, in CFG.Base]
incl_rcons [lemma, in CFG.Base]
incl_sing [lemma, in CFG.Base]
incl_lcons [lemma, in CFG.Base]
incl_shift [lemma, in CFG.Base]
incl_nil_eq [lemma, in CFG.Base]
incl_map [lemma, in CFG.Base]
incl_nil [lemma, in CFG.Base]
inlinable [inductive, in CFG.Inlining]
inlinable_cons [lemma, in CFG.Inlining]
Inlining [library]
inlL [definition, in CFG.Inlining]
inlL_langauge_equiv [lemma, in CFG.Inlining]
inlL_dom [lemma, in CFG.Inlining]
inlL_skip [lemma, in CFG.Inlining]
inl_language_equiv [lemma, in CFG.Inlining]
inN [constructor, in CFG.Inlining]
inR [constructor, in CFG.Inlining]
in_substG_der [lemma, in CFG.Inlining]
in_rem_iff [lemma, in CFG.Base]
in_filter_iff [lemma, in CFG.Base]
in_equi_proper [instance, in CFG.Base]
in_incl_proper [instance, in CFG.Base]
in_cons_neq [lemma, in CFG.Base]
in_sing [lemma, in CFG.Base]
it [definition, in CFG.Base]
item [definition, in CFG.Dec_Word]
items [definition, in CFG.Dec_Word]
items_refl [lemma, in CFG.Dec_Word]
Iteration [section, in CFG.Base]
Iteration.f [variable, in CFG.Base]
Iteration.X [variable, in CFG.Base]
it_fp [lemma, in CFG.Base]
it_ind [lemma, in CFG.Base]
L
language [definition, in CFG.Derivation]language_normalform [lemma, in CFG.Chomsky]
lang_dec [instance, in CFG.Dec_Word]
Lists [library]
list_cc [lemma, in CFG.Base]
list_exists_not_incl [lemma, in CFG.Base]
list_exists_DM [lemma, in CFG.Base]
list_exists_dec [instance, in CFG.Base]
list_forall_dec [instance, in CFG.Base]
list_sigma_forall [lemma, in CFG.Base]
list_in_dec [instance, in CFG.Base]
list_eq_dec [instance, in CFG.Base]
list_cycle [lemma, in CFG.Base]
list_unit [lemma, in CFG.Lists]
M
maxSymb [definition, in CFG.Symbols]maxSymbRule [definition, in CFG.Symbols]
maxSymbRule_corr [lemma, in CFG.Symbols]
maxSymb_corr [lemma, in CFG.Symbols]
Membership [section, in CFG.Base]
Membership.X [variable, in CFG.Base]
N
N [definition, in CFG.ElimU]nat_le_dec [instance, in CFG.Base]
nat_eq_dec [instance, in CFG.Base]
normalize [definition, in CFG.Chomsky]
not_in_cons [lemma, in CFG.Base]
not_dec [instance, in CFG.Base]
Null [constructor, in CFG.ElimE]
nullable [inductive, in CFG.ElimE]
nullable_eclosure [lemma, in CFG.ElimE]
nullable_dec [instance, in CFG.ElimE]
nullable_derE_equi [lemma, in CFG.ElimE]
nullable_derE [lemma, in CFG.ElimE]
O
or_dec [instance, in CFG.Base]P
P [definition, in CFG.Dec_Empty]phrase [definition, in CFG.Definitions]
phrase_char_dec [instance, in CFG.Definitions]
phrase_var_dec [instance, in CFG.Definitions]
pickChar [lemma, in CFG.Separate]
pickCharRule [lemma, in CFG.Separate]
pickFresh [lemma, in CFG.Symbols]
power [definition, in CFG.Base]
PowerRep [section, in CFG.Base]
PowerRep.X [variable, in CFG.Base]
power_extensional [lemma, in CFG.Base]
power_nil [lemma, in CFG.Base]
power_incl [lemma, in CFG.Base]
product [definition, in CFG.Lists]
productive [inductive, in CFG.Dec_Empty]
productive_dec [instance, in CFG.Dec_Empty]
productive_P [lemma, in CFG.Dec_Empty]
productive_derWord_equi [lemma, in CFG.Dec_Empty]
productive_derf [lemma, in CFG.Dec_Empty]
prod_corr [lemma, in CFG.Lists]
prod_corr2 [lemma, in CFG.Lists]
prod_corr1 [lemma, in CFG.Lists]
P_productive_equiv [lemma, in CFG.Dec_Empty]
P_productive [lemma, in CFG.Dec_Empty]
R
R [constructor, in CFG.Definitions]ran [definition, in CFG.Symbols]
ranG_rule [lemma, in CFG.Symbols]
ran_elimU_G [lemma, in CFG.ElimU]
rDer [constructor, in CFG.Derivation]
rem [definition, in CFG.Base]
Removal [section, in CFG.Base]
Removal.X [variable, in CFG.Base]
rem_inclr [lemma, in CFG.Base]
rem_reorder [lemma, in CFG.Base]
rem_id [lemma, in CFG.Base]
rem_fst' [lemma, in CFG.Base]
rem_fst [lemma, in CFG.Base]
rem_comm [lemma, in CFG.Base]
rem_equi [lemma, in CFG.Base]
rem_app' [lemma, in CFG.Base]
rem_app [lemma, in CFG.Base]
rem_neq [lemma, in CFG.Base]
rem_in [lemma, in CFG.Base]
rem_cons' [lemma, in CFG.Base]
rem_cons [lemma, in CFG.Base]
rem_mono [lemma, in CFG.Base]
rem_incl [lemma, in CFG.Base]
rem_not_in [lemma, in CFG.Base]
rep [definition, in CFG.Base]
replN [constructor, in CFG.Derivation]
rep_dupfree [lemma, in CFG.Base]
rep_idempotent [lemma, in CFG.Base]
rep_injective [lemma, in CFG.Base]
rep_eq [lemma, in CFG.Base]
rep_eq' [lemma, in CFG.Base]
rep_mono [lemma, in CFG.Base]
rep_equi [lemma, in CFG.Base]
rep_in [lemma, in CFG.Base]
rep_incl [lemma, in CFG.Base]
rep_power [lemma, in CFG.Base]
rule [inductive, in CFG.Definitions]
rules [definition, in CFG.ElimU]
rule_domVG [lemma, in CFG.ElimU]
rule_eq_dec [instance, in CFG.Definitions]
rule_ranG [lemma, in CFG.Symbols]
rule_domG [lemma, in CFG.Symbols]
S
sDer [constructor, in CFG.Derivation]segment [definition, in CFG.Lists]
segment_trans [lemma, in CFG.Lists]
segment_refl [lemma, in CFG.Lists]
segment_nil [lemma, in CFG.Lists]
segms [definition, in CFG.Lists]
segms_corr [lemma, in CFG.Lists]
segms_corr2 [lemma, in CFG.Lists]
segms_corr1 [lemma, in CFG.Lists]
sep [definition, in CFG.Separate]
Separate [library]
sep_language [lemma, in CFG.Separate]
sep_der_equiv [lemma, in CFG.Separate]
sep_uniform [lemma, in CFG.Separate]
size_recursion [lemma, in CFG.Base]
sless [definition, in CFG.Symbols]
sless_monotone [lemma, in CFG.Symbols]
sless_dec [instance, in CFG.Symbols]
sless' [definition, in CFG.Symbols]
slist [inductive, in CFG.Lists]
slists [definition, in CFG.Lists]
slists_slist [lemma, in CFG.Lists]
slist_pred [lemma, in CFG.Lists]
slist_length [lemma, in CFG.Lists]
slist_subsumes [lemma, in CFG.Lists]
slist_split [lemma, in CFG.Lists]
slist_inv [lemma, in CFG.Lists]
slist_equiv_pred [lemma, in CFG.Lists]
slist_append [lemma, in CFG.Lists]
slist_trans [lemma, in CFG.Lists]
slist_id [lemma, in CFG.Lists]
slist_closure_equiv [lemma, in CFG.ElimE]
slist_closure [lemma, in CFG.ElimE]
snds [definition, in CFG.Lists]
snds_split [lemma, in CFG.Lists]
splitList_dec [instance, in CFG.Lists]
step [definition, in CFG.Binarize]
step [definition, in CFG.Separate]
step [definition, in CFG.ElimU]
step [definition, in CFG.Dec_Empty]
step [definition, in CFG.Dec_Word]
step_dom [lemma, in CFG.Binarize]
step_der_equiv [lemma, in CFG.Binarize]
step_or [lemma, in CFG.Binarize]
step_dom [lemma, in CFG.Separate]
step_der_equiv [lemma, in CFG.Separate]
step_dec [instance, in CFG.ElimU]
step_dec' [instance, in CFG.ElimU]
step_dec [instance, in CFG.Dec_Empty]
step_dec [instance, in CFG.Dec_Word]
step_dec' [instance, in CFG.Dec_Word]
step' [definition, in CFG.Binarize]
subcons [constructor, in CFG.Lists]
subconsp [constructor, in CFG.Lists]
subnil [constructor, in CFG.Lists]
substG [definition, in CFG.Inlining]
substG_der_equiv [lemma, in CFG.Separate]
substG_dom [lemma, in CFG.Inlining]
substG_inG [lemma, in CFG.Inlining]
substG_undo [lemma, in CFG.Inlining]
substG_skip [lemma, in CFG.Inlining]
substG_skipRule [lemma, in CFG.Inlining]
substG_split [lemma, in CFG.Inlining]
substG_preservesLength [lemma, in CFG.Chomsky]
substL [definition, in CFG.Lists]
substL_der [lemma, in CFG.Inlining]
substL_undo [lemma, in CFG.Lists]
substL_length_unit [lemma, in CFG.Lists]
substL_skip [lemma, in CFG.Lists]
substL_split [lemma, in CFG.Lists]
symbol [inductive, in CFG.Definitions]
Symbols [library]
symbol_ter_dec [instance, in CFG.Definitions]
symbol_eq_dec [instance, in CFG.Definitions]
symbs [definition, in CFG.Symbols]
symbs_der [lemma, in CFG.Derivation]
symbs_subset [lemma, in CFG.Symbols]
symbs_inv [lemma, in CFG.Symbols]
symbs_dom [lemma, in CFG.Symbols]
T
T [constructor, in CFG.Definitions]ter [inductive, in CFG.Definitions]
terminal [definition, in CFG.Derivation]
terminal_split [lemma, in CFG.Derivation]
TProd [constructor, in CFG.Dec_Empty]
True_dec [instance, in CFG.Base]
Ts [constructor, in CFG.Definitions]
U
undup [definition, in CFG.Base]Undup [section, in CFG.Base]
undup_idempotent [lemma, in CFG.Base]
undup_id [lemma, in CFG.Base]
undup_equi [lemma, in CFG.Base]
undup_incl [lemma, in CFG.Base]
undup_id_equi [lemma, in CFG.Base]
Undup.X [variable, in CFG.Base]
uniform [definition, in CFG.Separate]
unitfree [definition, in CFG.ElimU]
unitfree_elimU [lemma, in CFG.ElimU]
unitfree_elimU' [lemma, in CFG.ElimU]
UnitRules [section, in CFG.ElimU]
UnitRules.G [variable, in CFG.ElimU]
unit_language [lemma, in CFG.ElimU]
V
V [constructor, in CFG.Definitions]var [inductive, in CFG.Definitions]
var_eq_dec [instance, in CFG.Definitions]
vDer [constructor, in CFG.Derivation]
VProd [constructor, in CFG.Dec_Empty]
Vs [constructor, in CFG.Definitions]
other
_ === _ [notation, in CFG.Base]_ <<= _ [notation, in CFG.Base]
_ el _ [notation, in CFG.Base]
eq_dec _ [notation, in CFG.Base]
| _ | [notation, in CFG.Base]
Notation Index
other
_ === _ [in CFG.Base]_ <<= _ [in CFG.Base]
_ el _ [in CFG.Base]
eq_dec _ [in CFG.Base]
| _ | [in CFG.Base]
Module Index
F
FCI [in CFG.Base]Variable Index
C
Cardinality.X [in CFG.Base]D
Dec_Emptys.G [in CFG.Dec_Empty]Dec_Word.u [in CFG.Dec_Word]
Dec_Word.G [in CFG.Dec_Word]
DelE.G [in CFG.ElimE]
Dupfree.X [in CFG.Base]
E
EClosure.G [in CFG.ElimE]Equi.X [in CFG.Base]
F
FCI.FCI.step [in CFG.Base]FCI.FCI.V [in CFG.Base]
FCI.FCI.X [in CFG.Base]
FilterComm.p [in CFG.Base]
FilterComm.q [in CFG.Base]
FilterComm.X [in CFG.Base]
FilterLemmas_pq.q [in CFG.Base]
FilterLemmas_pq.p [in CFG.Base]
FilterLemmas_pq.X [in CFG.Base]
FilterLemmas.p [in CFG.Base]
FilterLemmas.X [in CFG.Base]
I
Inclusion.X [in CFG.Base]Iteration.f [in CFG.Base]
Iteration.X [in CFG.Base]
M
Membership.X [in CFG.Base]P
PowerRep.X [in CFG.Base]R
Removal.X [in CFG.Base]U
Undup.X [in CFG.Base]UnitRules.G [in CFG.ElimU]
Library Index
B
BaseBinarize
C
ChomskyD
Dec_WordDec_Empty
Definitions
Derivation
E
ElimEElimU
I
InliningL
ListsS
SeparateSymbols
Lemma Index
B
binary_unit [in CFG.Chomsky]binary_elimE [in CFG.Chomsky]
binary_sep [in CFG.Chomsky]
bin_language [in CFG.Binarize]
bin_der_equiv [in CFG.Binarize]
bin_binary [in CFG.Binarize]
bin_dom [in CFG.Chomsky]
C
card_or [in CFG.Base]card_lt [in CFG.Base]
card_equi [in CFG.Base]
card_ex [in CFG.Base]
card_0 [in CFG.Base]
card_cons_rem [in CFG.Base]
card_eq [in CFG.Base]
card_le [in CFG.Base]
card_not_in_rem [in CFG.Base]
card_in_rem [in CFG.Base]
chomsky_normalform [in CFG.Chomsky]
closure_slist [in CFG.ElimE]
concat_split [in CFG.Lists]
count_decr [in CFG.Binarize]
count_decr [in CFG.Separate]
count_sep_decr [in CFG.Separate]
count_chars_decr [in CFG.Separate]
count_chars_split [in CFG.Separate]
count_sep_substL [in CFG.Separate]
count_chars_substL [in CFG.Separate]
count_sep_split [in CFG.Separate]
D
dec_prop_iff [in CFG.Base]dec_DM_impl [in CFG.Base]
dec_DM_and [in CFG.Base]
dec_DN [in CFG.Base]
delE_der_equiv [in CFG.ElimE]
delE_rules [in CFG.ElimE]
delE_preserveG [in CFG.ElimE]
delE_efree [in CFG.ElimE]
derE_nullable [in CFG.ElimE]
derfelimU_derfG [in CFG.ElimU]
derfG_derfelimU [in CFG.ElimU]
derf_der_equiv [in CFG.Derivation]
derf_derT [in CFG.Derivation]
derf_trans [in CFG.Derivation]
derf_split [in CFG.Derivation]
derf_concat [in CFG.Derivation]
derf_productive [in CFG.Dec_Empty]
derf_DW [in CFG.Dec_Word]
derI_derf [in CFG.Derivation]
derL_der_equiv [in CFG.Derivation]
derT_concat [in CFG.Derivation]
derT_trans [in CFG.Derivation]
derT_derI [in CFG.Derivation]
derT_der_equiv [in CFG.Derivation]
derT_slist [in CFG.ElimE]
der_equiv_G [in CFG.Derivation]
der_subset [in CFG.Derivation]
der_G_inlL [in CFG.Inlining]
der_inlL_G [in CFG.Inlining]
der_inlL_G' [in CFG.Inlining]
der_substG_G_equiv [in CFG.Inlining]
der_G_substG [in CFG.Inlining]
der_G_substG' [in CFG.Inlining]
der_substG_G [in CFG.Inlining]
der_G_delE [in CFG.ElimE]
der_eclosure_equiv [in CFG.ElimE]
disjoint_cons [in CFG.Base]
disjoint_forall [in CFG.Base]
disjoint_incl [in CFG.Base]
disjoint_symm [in CFG.Base]
disjoint_nil' [in CFG.Base]
disjoint_nil [in CFG.Base]
domG_rule [in CFG.Symbols]
domVG_rule [in CFG.ElimU]
dom_domV [in CFG.ElimU]
dom_subset [in CFG.Symbols]
dupfree_in_power [in CFG.Base]
dupfree_power [in CFG.Base]
dupfree_undup [in CFG.Base]
dupfree_card [in CFG.Base]
dupfree_dec [in CFG.Base]
dupfree_filter [in CFG.Base]
dupfree_map [in CFG.Base]
dupfree_app [in CFG.Base]
dupfree_cons [in CFG.Base]
DW_der_equiv [in CFG.Dec_Word]
DW_der_equiv' [in CFG.Dec_Word]
DW_derf' [in CFG.Dec_Word]
E
eclosed_eclosure [in CFG.ElimE]eclosure_der [in CFG.ElimE]
efree_unit [in CFG.Chomsky]
efree_elimE [in CFG.ElimE]
elimE_language [in CFG.ElimE]
elimU_der_equiv [in CFG.ElimU]
elimU_corr3 [in CFG.ElimU]
elimU_corr3' [in CFG.ElimU]
elimU_corr2 [in CFG.ElimU]
elimU_corr [in CFG.ElimU]
equi_rotate [in CFG.Base]
equi_shift [in CFG.Base]
equi_swap [in CFG.Base]
equi_dup [in CFG.Base]
equi_push [in CFG.Base]
excluded_unit [in CFG.Chomsky]
excluded_free [in CFG.Chomsky]
F
FCI.closure [in CFG.Base]FCI.fp [in CFG.Base]
FCI.incl [in CFG.Base]
FCI.ind [in CFG.Base]
FCI.it_incl [in CFG.Base]
FCI.pick [in CFG.Base]
filter_comm [in CFG.Base]
filter_and [in CFG.Base]
filter_pq_eq [in CFG.Base]
filter_pq_mono [in CFG.Base]
filter_fst' [in CFG.Base]
filter_fst [in CFG.Base]
filter_app [in CFG.Base]
filter_id [in CFG.Base]
filter_mono [in CFG.Base]
filter_incl [in CFG.Base]
fp_binary [in CFG.Binarize]
fp_bin [in CFG.Binarize]
fp_uniform [in CFG.Separate]
fp_sep [in CFG.Separate]
fresh_symbs [in CFG.Symbols]
fsts_split [in CFG.Lists]
fsts_comb_corr [in CFG.Dec_Word]
fsts_comb_corr2 [in CFG.Dec_Word]
fsts_comb_corr1 [in CFG.Dec_Word]
I
incl_app_left [in CFG.Base]incl_lrcons [in CFG.Base]
incl_rcons [in CFG.Base]
incl_sing [in CFG.Base]
incl_lcons [in CFG.Base]
incl_shift [in CFG.Base]
incl_nil_eq [in CFG.Base]
incl_map [in CFG.Base]
incl_nil [in CFG.Base]
inlinable_cons [in CFG.Inlining]
inlL_langauge_equiv [in CFG.Inlining]
inlL_dom [in CFG.Inlining]
inlL_skip [in CFG.Inlining]
inl_language_equiv [in CFG.Inlining]
in_substG_der [in CFG.Inlining]
in_rem_iff [in CFG.Base]
in_filter_iff [in CFG.Base]
in_cons_neq [in CFG.Base]
in_sing [in CFG.Base]
items_refl [in CFG.Dec_Word]
it_fp [in CFG.Base]
it_ind [in CFG.Base]
L
language_normalform [in CFG.Chomsky]list_cc [in CFG.Base]
list_exists_not_incl [in CFG.Base]
list_exists_DM [in CFG.Base]
list_sigma_forall [in CFG.Base]
list_cycle [in CFG.Base]
list_unit [in CFG.Lists]
M
maxSymbRule_corr [in CFG.Symbols]maxSymb_corr [in CFG.Symbols]
N
not_in_cons [in CFG.Base]nullable_eclosure [in CFG.ElimE]
nullable_derE_equi [in CFG.ElimE]
nullable_derE [in CFG.ElimE]
P
pickChar [in CFG.Separate]pickCharRule [in CFG.Separate]
pickFresh [in CFG.Symbols]
power_extensional [in CFG.Base]
power_nil [in CFG.Base]
power_incl [in CFG.Base]
productive_P [in CFG.Dec_Empty]
productive_derWord_equi [in CFG.Dec_Empty]
productive_derf [in CFG.Dec_Empty]
prod_corr [in CFG.Lists]
prod_corr2 [in CFG.Lists]
prod_corr1 [in CFG.Lists]
P_productive_equiv [in CFG.Dec_Empty]
P_productive [in CFG.Dec_Empty]
R
ranG_rule [in CFG.Symbols]ran_elimU_G [in CFG.ElimU]
rem_inclr [in CFG.Base]
rem_reorder [in CFG.Base]
rem_id [in CFG.Base]
rem_fst' [in CFG.Base]
rem_fst [in CFG.Base]
rem_comm [in CFG.Base]
rem_equi [in CFG.Base]
rem_app' [in CFG.Base]
rem_app [in CFG.Base]
rem_neq [in CFG.Base]
rem_in [in CFG.Base]
rem_cons' [in CFG.Base]
rem_cons [in CFG.Base]
rem_mono [in CFG.Base]
rem_incl [in CFG.Base]
rem_not_in [in CFG.Base]
rep_dupfree [in CFG.Base]
rep_idempotent [in CFG.Base]
rep_injective [in CFG.Base]
rep_eq [in CFG.Base]
rep_eq' [in CFG.Base]
rep_mono [in CFG.Base]
rep_equi [in CFG.Base]
rep_in [in CFG.Base]
rep_incl [in CFG.Base]
rep_power [in CFG.Base]
rule_domVG [in CFG.ElimU]
rule_ranG [in CFG.Symbols]
rule_domG [in CFG.Symbols]
S
segment_trans [in CFG.Lists]segment_refl [in CFG.Lists]
segment_nil [in CFG.Lists]
segms_corr [in CFG.Lists]
segms_corr2 [in CFG.Lists]
segms_corr1 [in CFG.Lists]
sep_language [in CFG.Separate]
sep_der_equiv [in CFG.Separate]
sep_uniform [in CFG.Separate]
size_recursion [in CFG.Base]
sless_monotone [in CFG.Symbols]
slists_slist [in CFG.Lists]
slist_pred [in CFG.Lists]
slist_length [in CFG.Lists]
slist_subsumes [in CFG.Lists]
slist_split [in CFG.Lists]
slist_inv [in CFG.Lists]
slist_equiv_pred [in CFG.Lists]
slist_append [in CFG.Lists]
slist_trans [in CFG.Lists]
slist_id [in CFG.Lists]
slist_closure_equiv [in CFG.ElimE]
slist_closure [in CFG.ElimE]
snds_split [in CFG.Lists]
step_dom [in CFG.Binarize]
step_der_equiv [in CFG.Binarize]
step_or [in CFG.Binarize]
step_dom [in CFG.Separate]
step_der_equiv [in CFG.Separate]
substG_der_equiv [in CFG.Separate]
substG_dom [in CFG.Inlining]
substG_inG [in CFG.Inlining]
substG_undo [in CFG.Inlining]
substG_skip [in CFG.Inlining]
substG_skipRule [in CFG.Inlining]
substG_split [in CFG.Inlining]
substG_preservesLength [in CFG.Chomsky]
substL_der [in CFG.Inlining]
substL_undo [in CFG.Lists]
substL_length_unit [in CFG.Lists]
substL_skip [in CFG.Lists]
substL_split [in CFG.Lists]
symbs_der [in CFG.Derivation]
symbs_subset [in CFG.Symbols]
symbs_inv [in CFG.Symbols]
symbs_dom [in CFG.Symbols]
T
terminal_split [in CFG.Derivation]U
undup_idempotent [in CFG.Base]undup_id [in CFG.Base]
undup_equi [in CFG.Base]
undup_incl [in CFG.Base]
undup_id_equi [in CFG.Base]
unitfree_elimU [in CFG.ElimU]
unitfree_elimU' [in CFG.ElimU]
unit_language [in CFG.ElimU]
Constructor Index
D
derIRefl [in CFG.Derivation]derIRule [in CFG.Derivation]
derITrans [in CFG.Derivation]
derTRefl [in CFG.Derivation]
derTRule [in CFG.Derivation]
derTTrans [in CFG.Derivation]
dupfreeC [in CFG.Base]
dupfreeN [in CFG.Base]
F
fCons [in CFG.Derivation]fRefl [in CFG.Derivation]
fRule [in CFG.Derivation]
G
gDer [in CFG.Derivation]I
inN [in CFG.Inlining]inR [in CFG.Inlining]
N
Null [in CFG.ElimE]R
R [in CFG.Definitions]rDer [in CFG.Derivation]
replN [in CFG.Derivation]
S
sDer [in CFG.Derivation]subcons [in CFG.Lists]
subconsp [in CFG.Lists]
subnil [in CFG.Lists]
T
T [in CFG.Definitions]TProd [in CFG.Dec_Empty]
Ts [in CFG.Definitions]
V
V [in CFG.Definitions]vDer [in CFG.Derivation]
VProd [in CFG.Dec_Empty]
Vs [in CFG.Definitions]
Inductive Index
D
der [in CFG.Derivation]derf [in CFG.Derivation]
derI [in CFG.Derivation]
derL [in CFG.Derivation]
derT [in CFG.Derivation]
dupfree [in CFG.Base]
I
inlinable [in CFG.Inlining]N
nullable [in CFG.ElimE]P
productive [in CFG.Dec_Empty]R
rule [in CFG.Definitions]S
slist [in CFG.Lists]symbol [in CFG.Definitions]
T
ter [in CFG.Definitions]V
var [in CFG.Definitions]Instance Index
A
and_dec [in CFG.Base]app_equi_proper [in CFG.Base]
app_incl_proper [in CFG.Base]
B
bool_eq_dec [in CFG.Base]C
card_equi_proper [in CFG.Base]cons_equi_proper [in CFG.Base]
cons_incl_proper [in CFG.Base]
D
dec_charfree [in CFG.Separate]der_dec [in CFG.Dec_Word]
E
equi_Equivalence [in CFG.Base]eq_dec_prod [in CFG.Lists]
exists_phrase_dec [in CFG.Definitions]
exists_rule_dec [in CFG.Definitions]
exists_dec [in CFG.Dec_Empty]
F
False_dec [in CFG.Base]filter_rule_dec [in CFG.Definitions]
filter_prod_dec [in CFG.Lists]
I
iff_dec [in CFG.Base]impl_dec [in CFG.Base]
incl_equi_proper [in CFG.Base]
incl_preorder [in CFG.Base]
in_equi_proper [in CFG.Base]
in_incl_proper [in CFG.Base]
L
lang_dec [in CFG.Dec_Word]list_exists_dec [in CFG.Base]
list_forall_dec [in CFG.Base]
list_in_dec [in CFG.Base]
list_eq_dec [in CFG.Base]
N
nat_le_dec [in CFG.Base]nat_eq_dec [in CFG.Base]
not_dec [in CFG.Base]
nullable_dec [in CFG.ElimE]
O
or_dec [in CFG.Base]P
phrase_char_dec [in CFG.Definitions]phrase_var_dec [in CFG.Definitions]
productive_dec [in CFG.Dec_Empty]
R
rule_eq_dec [in CFG.Definitions]S
sless_dec [in CFG.Symbols]splitList_dec [in CFG.Lists]
step_dec [in CFG.ElimU]
step_dec' [in CFG.ElimU]
step_dec [in CFG.Dec_Empty]
step_dec [in CFG.Dec_Word]
step_dec' [in CFG.Dec_Word]
symbol_ter_dec [in CFG.Definitions]
symbol_eq_dec [in CFG.Definitions]
T
True_dec [in CFG.Base]V
var_eq_dec [in CFG.Definitions]Section Index
C
Cardinality [in CFG.Base]D
Dec_Emptys [in CFG.Dec_Empty]Dec_Word [in CFG.Dec_Word]
DelE [in CFG.ElimE]
Dupfree [in CFG.Base]
E
EClosure [in CFG.ElimE]Equi [in CFG.Base]
F
FCI.FCI [in CFG.Base]FilterComm [in CFG.Base]
FilterLemmas [in CFG.Base]
FilterLemmas_pq [in CFG.Base]
I
Inclusion [in CFG.Base]Iteration [in CFG.Base]
M
Membership [in CFG.Base]P
PowerRep [in CFG.Base]R
Removal [in CFG.Base]U
Undup [in CFG.Base]UnitRules [in CFG.ElimU]
Definition Index
B
bin [in CFG.Binarize]binary [in CFG.Binarize]
C
card [in CFG.Base]charfree [in CFG.Separate]
chomsky [in CFG.Chomsky]
closure [in CFG.ElimE]
concat [in CFG.Lists]
count_bin [in CFG.Binarize]
count_sep [in CFG.Separate]
count_chars [in CFG.Separate]
D
dec [in CFG.Base]decision [in CFG.Base]
delE [in CFG.ElimE]
disjoint [in CFG.Base]
dom [in CFG.Symbols]
domV [in CFG.ElimU]
dupfree_inv [in CFG.Base]
DW [in CFG.Dec_Word]
E
eclosed [in CFG.ElimE]eclosure [in CFG.ElimE]
efree [in CFG.ElimE]
elimE [in CFG.ElimE]
elimU [in CFG.ElimU]
equi [in CFG.Base]
F
FCI.C [in CFG.Base]FCI.F [in CFG.Base]
filter [in CFG.Base]
FP [in CFG.Base]
fresh [in CFG.Symbols]
fsts [in CFG.Lists]
fsts_comb [in CFG.Dec_Word]
G
getNat [in CFG.Symbols]grammar [in CFG.Definitions]
I
inclp [in CFG.Base]inlL [in CFG.Inlining]
it [in CFG.Base]
item [in CFG.Dec_Word]
items [in CFG.Dec_Word]
L
language [in CFG.Derivation]M
maxSymb [in CFG.Symbols]maxSymbRule [in CFG.Symbols]
N
N [in CFG.ElimU]normalize [in CFG.Chomsky]
P
P [in CFG.Dec_Empty]phrase [in CFG.Definitions]
power [in CFG.Base]
product [in CFG.Lists]
R
ran [in CFG.Symbols]rem [in CFG.Base]
rep [in CFG.Base]
rules [in CFG.ElimU]
S
segment [in CFG.Lists]segms [in CFG.Lists]
sep [in CFG.Separate]
sless [in CFG.Symbols]
sless' [in CFG.Symbols]
slists [in CFG.Lists]
snds [in CFG.Lists]
step [in CFG.Binarize]
step [in CFG.Separate]
step [in CFG.ElimU]
step [in CFG.Dec_Empty]
step [in CFG.Dec_Word]
step' [in CFG.Binarize]
substG [in CFG.Inlining]
substL [in CFG.Lists]
symbs [in CFG.Symbols]
T
terminal [in CFG.Derivation]U
undup [in CFG.Base]uniform [in CFG.Separate]
unitfree [in CFG.ElimU]
| 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 | (489 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 | (5 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (27 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 | (13 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 | (263 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 | (29 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 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 | (18 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 | (71 entries) |